:: On the Monoid of Endomorphisms of Universal Algebra \& Many
:: Sorted Algebra
::  by Jaros{\l}aw Gryko
::
:: Received October 17, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies UNIALG_1, FUNCT_2, STRUCT_0, FUNCT_1, MSUALG_3, SUBSET_1,
      RELAT_1, XBOOLE_0, TARSKI, BINOP_1, ALGSTR_0, MESFUNC1, VECTSP_1,
      GROUP_1, MSUALG_1, AUTALG_1, PBOOLE, MEMBER_1, CARD_1,
      FUNCOP_1, MSUHOM_1, MSSUBFAM, GROUP_6, WELLORD1, ZFMISC_1, ENDALG;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE,
      CARD_3, BINOP_1, PARTFUN1, FUNCT_2, FUNCOP_1, NUMBERS, STRUCT_0,
      ALGSTR_0, GROUP_1, VECTSP_1, FINSEQ_1, PZFMISC1, UNIALG_1, MSUALG_1,
      ALG_1, MSUALG_3, MSUHOM_1, AUTALG_1, GROUP_6;
 constructors BINOP_1, CARD_3, PZFMISC1, VECTSP_1, GROUP_6, ALG_1, MSUALG_3,
      MSUHOM_1, AUTALG_1, RELSET_1;
 registrations XBOOLE_0, FUNCT_1, ORDINAL1, FUNCT_2, PBOOLE, STRUCT_0,
      VECTSP_1, MSUALG_1, ALGSTR_0, RELSET_1, AUTALG_1;
 requirements SUBSET, BOOLE;
 definitions AUTALG_1, FUNCT_1, TARSKI, VECTSP_1, XBOOLE_0, GROUP_1, FUNCOP_1,
      STRUCT_0, ALGSTR_0, FUNCT_2;
 theorems AUTALG_1, ALG_1, BINOP_1, FUNCOP_1, FUNCT_1, FUNCT_2, GROUP_6,
      MSUALG_1, MSUALG_3, MSUHOM_1, TARSKI, ZFMISC_1, RELAT_1, VECTSP_1,
      RELSET_1, XBOOLE_0, GROUP_1, PBOOLE;
 schemes BINOP_1, FUNCT_1, XBOOLE_0;

begin

reserve UA for Universal_Algebra;

definition
  let UA;
  func UAEnd UA -> FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
  means
  :Def1:
  for h be Function of UA, UA holds h in it iff h is_homomorphism UA , UA;
  existence
  proof
    set F = {x where x is Element of Funcs (the carrier of UA, the carrier of
    UA): x is_homomorphism UA, UA};
A1: id the carrier of UA in F
    proof
      set I = id the carrier of UA;
      I in Funcs (the carrier of UA, the carrier of UA) & I
      is_homomorphism UA, UA by ALG_1:5,FUNCT_2:8;
      hence thesis;
    end;
    F is functional
    proof
      let q be set;
      assume q in F;
      then
      ex x be Element of Funcs(the carrier of UA, the carrier of UA ) st q
      = x & x is_homomorphism UA, UA;
      hence thesis;
    end;
    then reconsider F as functional non empty set by A1;
    F is FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
    proof
      let a be Element of F;
      a in F;
      then
      ex x be Element of Funcs(the carrier of UA, the carrier of UA ) st a
      = x & x is_homomorphism UA, UA;
      hence thesis;
    end;
    then reconsider
    F as FUNCTION_DOMAIN of the carrier of UA, the carrier of UA;
    take F;
    let h be Function of UA, UA;
    thus h in F implies h is_homomorphism UA, UA
    proof
      assume h in F;
      then ex f be Element of Funcs (the carrier of UA, the carrier of UA) st
      f = h & f is_homomorphism UA, UA;
      hence thesis;
    end;
A2: h is Element of Funcs (the carrier of UA, the carrier of UA) by FUNCT_2:8;
    assume h is_homomorphism UA, UA;
    hence thesis by A2;
  end;
  uniqueness
  proof
    let F1,F2 be FUNCTION_DOMAIN of the carrier of UA,the carrier of UA;
    assume that
A3: for h be Function of UA, UA holds h in F1 iff h is_homomorphism UA, UA and
A4: for h be Function of UA, UA holds h in F2 iff h is_homomorphism UA, UA;
A5: for f be Element of F2 holds f is Function of UA, UA;
A6: F2 c= F1
    proof
      let q be set;
      assume
A7:   q in F2;
      then reconsider h1 = q as Function of UA, UA by A5;
      h1 is_homomorphism UA, UA by A4,A7;
      hence thesis by A3;
    end;
A8: for f be Element of F1 holds f is Function of UA, UA;
    F1 c= F2
    proof
      let q be set;
      assume
A9:   q in F1;
      then reconsider h1 = q as Function of UA, UA by A8;
      h1 is_homomorphism UA, UA by A3,A9;
      hence thesis by A4;
    end;
    hence thesis by A6,XBOOLE_0:def 10;
  end;
end;

theorem
  UAEnd UA c= Funcs (the carrier of UA, the carrier of UA)
proof
  let q be set;
  assume q in UAEnd UA;
  then q is Element of UAEnd UA;
  hence thesis by FUNCT_2:9;
end;

theorem Th2:
  id the carrier of UA in UAEnd UA
proof
  id the carrier of UA is_homomorphism UA, UA by ALG_1:5;
  hence thesis by Def1;
end;

theorem Th3:
  for f1, f2 be Element of UAEnd UA holds f1 * f2 in UAEnd UA
proof
  let f1, f2 be Element of UAEnd UA;
  f1 is_homomorphism UA, UA & f2 is_homomorphism UA, UA by Def1;
  then f1 * f2 is_homomorphism UA, UA by ALG_1:6;
  hence thesis by Def1;
end;

definition
  let UA;
  func UAEndComp UA -> BinOp of UAEnd UA means
  :Def2:
  for x, y be Element of UAEnd UA holds it.(x, y) = y * x;
  existence
  proof
    defpred P[Element of UAEnd UA, Element of UAEnd UA, set] means $3 = $2 *
    $1;
A1: for x, y be Element of UAEnd UA ex m be Element of UAEnd UA st P[x,y,m ]
    proof
      let x, y be Element of UAEnd UA;
      reconsider xx = x, yy = y as Function of UA, UA;
      reconsider m = yy * xx as Element of UAEnd UA by Th3;
      take m;
      thus thesis;
    end;
    ex B being BinOp of UAEnd UA st for x, y be Element of UAEnd UA holds
    P[x,y,B.(x, y)] from BINOP_1:sch 3(A1);
    hence thesis;
  end;
  uniqueness
  proof
    let b1, b2 be BinOp of UAEnd UA such that
A2: for x, y be Element of UAEnd UA holds b1.(x, y) = y * x and
A3: for x, y be Element of UAEnd UA holds b2.(x, y) = y * x;
    for x, y be Element of UAEnd UA holds b1.(x, y) = b2.(x, y)
    proof
      let x, y be Element of UAEnd UA;
      thus b1.(x, y) = y * x by A2
        .= b2.(x, y) by A3;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

definition
  let UA;
  func UAEndMonoid UA -> strict multLoopStr means
  :Def3:
  the carrier of it = UAEnd UA &
  the multF of it = UAEndComp UA & 1.it = id the carrier of UA;
  existence
  proof
    reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
    take multLoopStr(#UAEnd UA, UAEndComp UA, i#);
    thus thesis;
  end;
  uniqueness;
end;

registration
  let UA;
  cluster UAEndMonoid UA -> non empty;
  coherence
  proof
    reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
    set M = multLoopStr(#UAEnd UA, UAEndComp UA, i#);
    1.M = i;
    hence thesis by Def3;
  end;
end;

Lm1: now
  let UA;
  let x, e be Element of UAEndMonoid UA;
  reconsider i = e, y = x as Element of UAEnd UA by Def3;
  assume
A1: e = id the carrier of UA;
  thus x*e = (UAEndComp UA).(y,i) by Def3
    .= i*y by Def2
    .= x by A1,FUNCT_2:17;
  thus e*x = (UAEndComp UA).(i,y) by Def3
    .= y*i by Def2
    .= x by A1,FUNCT_2:17;
end;

registration
  let UA;
  cluster UAEndMonoid UA -> well-unital associative;
  coherence
  proof
    reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
    set H = multLoopStr (# UAEnd UA, UAEndComp UA, i#);
    thus UAEndMonoid UA is well-unital
    proof
      let x be Element of UAEndMonoid UA;
      1.UAEndMonoid UA = i by Def3;
      hence thesis by Lm1;
    end;
    for f, g, h be Element of H holds (f * g) * h = f * (g * h)
    proof
      let f, g, h be Element of H;
      reconsider A = f, B = g, C = h as Element of UAEnd UA;
A1:   g * h = C * B by Def2;
      f * g = B * A by Def2;
      hence (f * g) * h = C * (B * A) by Def2
        .= (C * B) * A by RELAT_1:36
        .= f * (g * h) by A1,Def2;
    end;
    then 1.H = i & H is associative by GROUP_1:def 3;
    hence thesis by Def3;
  end;
end;

theorem Th4:
  for x, y be Element of UAEndMonoid UA for f, g be Element of
  UAEnd UA st x = f & y = g holds x * y = g * f
proof
  reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
  let x, y be Element of UAEndMonoid UA;
  let f, g be Element of UAEnd UA;
  set H = multLoopStr (# UAEnd UA, UAEndComp UA,i #);
  1.H = i;
  then
A1: UAEndMonoid UA = H by Def3;
  assume x = f & y = g;
  hence thesis by A1,Def2;
end;

theorem
  id the carrier of UA = 1_UAEndMonoid UA by Def3;

reserve S for non void non empty ManySortedSign,
  U1 for non-empty MSAlgebra over S;

definition
  let S, U1;
  set T = the Sorts of U1;
  func MSAEnd U1 -> MSFunctionSet of U1,U1 means
  :Def4:
  (for f be Element of it holds f is ManySortedFunction of U1, U1) & for h
  be ManySortedFunction of U1, U1 holds h in it iff h is_homomorphism U1, U1;
  existence
  proof
    defpred P[set] means ex msf be ManySortedFunction of U1, U1 st $1 = msf &
    msf is_homomorphism U1, U1;
    consider X be set such that
A1: for x be set holds x in X iff x in MSFuncs(T,T) & P[x]
    from XBOOLE_0:sch 1;
    id T in MSFuncs(T,T) & ex F being ManySortedFunction of U1,
    U1 st id T = F & F is_homomorphism U1, U1 by AUTALG_1:20,MSUALG_3:9;
    then reconsider X as non empty set by A1;
    X c= MSFuncs(T,T)
    proof
      let q be set;
      thus thesis by A1;
    end;
    then reconsider X as MSFunctionSet of U1,U1;
    take X;
    thus for f be Element of X holds f is ManySortedFunction of U1, U1;
    let h be ManySortedFunction of U1, U1;
    hereby
      assume h in X;
      then ex msf be ManySortedFunction of U1, U1 st h = msf & msf
      is_homomorphism U1, U1 by A1;
      hence h is_homomorphism U1, U1;
    end;
    h in MSFuncs(T,T) by AUTALG_1:20;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let F1, F2 be MSFunctionSet of U1,U1 such that
A3: for f be Element of F1 holds f is ManySortedFunction of U1, U1 and
A4: for h be ManySortedFunction of U1, U1 holds h in F1 iff h
    is_homomorphism U1, U1 and
A5: for f be Element of F2 holds f is ManySortedFunction of U1, U1 and
A6: for h be ManySortedFunction of U1, U1 holds h in F2 iff h
    is_homomorphism U1, U1;
A7: F2 c= F1
    proof
      let q be set;
      assume
A8:   q in F2;
      then reconsider h1 = q as ManySortedFunction of U1, U1 by A5;
      h1 is_homomorphism U1, U1 by A6,A8;
      hence thesis by A4;
    end;
    F1 c= F2
    proof
      let q be set;
      assume
A9:   q in F1;
      then reconsider h1 = q as ManySortedFunction of U1, U1 by A3;
      h1 is_homomorphism U1, U1 by A4,A9;
      hence thesis by A6;
    end;
    hence thesis by A7,XBOOLE_0:def 10;
  end;
end;

theorem
  MSAEnd U1 c= MSFuncs(the Sorts of U1, the Sorts of U1);

theorem Th7:
  id the Sorts of U1 in MSAEnd U1
proof
  id the Sorts of U1 is_homomorphism U1, U1 by MSUALG_3:9;
  hence thesis by Def4;
end;

theorem Th8:
  for f1, f2 be Element of MSAEnd U1 holds f1 ** f2 in MSAEnd U1
proof
  let f1, f2 be Element of MSAEnd U1;
  f1 is_homomorphism U1, U1 & f2 is_homomorphism U1, U1 by Def4;
  then f1 ** f2 is_homomorphism U1, U1 by MSUALG_3:10;
  hence thesis by Def4;
end;

theorem Th9:
  for F be ManySortedFunction of MSAlg UA, MSAlg UA for f be
  Element of UAEnd UA st F = 0 .--> f holds F in MSAEnd MSAlg UA
proof
  let F be ManySortedFunction of MSAlg UA, MSAlg UA;
  let f be Element of UAEnd UA;
  assume F = 0 .--> f;
  then
A1: F = MSAlg f by MSUHOM_1:def 3;
  f is_homomorphism UA, UA by Def1;
  then MSAlg f is_homomorphism MSAlg UA, MSAlg UA Over MSSign UA by MSUHOM_1:16
;
  then F is_homomorphism MSAlg UA, MSAlg UA by A1,MSUHOM_1:9;
  hence thesis by Def4;
end;

definition
  let S, U1;
  func MSAEndComp U1 -> BinOp of MSAEnd U1 means
  :Def5:
  for x, y be Element of MSAEnd U1 holds it.(x, y) = y ** x;
  existence
  proof
    defpred P[Element of MSAEnd U1,Element of MSAEnd U1,set] means $3 = $2 **
    $1;
A1: for x, y be Element of MSAEnd U1 ex m be Element of MSAEnd U1 st P[x,y ,m]
    proof
      let x, y be Element of MSAEnd U1;
      reconsider xx = x, yy = y as ManySortedFunction of U1, U1;
      reconsider m = yy ** xx as Element of MSAEnd U1 by Th8;
      take m;
      thus thesis;
    end;
    ex B being BinOp of MSAEnd U1 st for x, y be Element of MSAEnd U1
    holds P[x,y,B.(x, y)] from BINOP_1:sch 3 (A1);
    hence thesis;
  end;
  uniqueness
  proof
    let b1, b2 be BinOp of MSAEnd U1 such that
A2: for x, y be Element of MSAEnd U1 holds b1.(x, y) = y ** x and
A3: for x, y be Element of MSAEnd U1 holds b2.(x, y) = y ** x;
    for x, y be Element of MSAEnd U1 holds b1.(x, y) = b2.(x, y)
    proof
      let x, y be Element of MSAEnd U1;
      thus b1.(x, y) = y ** x by A2
        .= b2.(x, y) by A3;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

definition
  let S, U1;
  func MSAEndMonoid U1 -> strict multLoopStr means
  :Def6:
  the carrier of it =
  MSAEnd U1 & the multF of it = MSAEndComp U1 & 1.it = id the Sorts of U1;
  existence
  proof
    reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7;
    take H = multLoopStr(#MSAEnd U1, MSAEndComp U1, i#);
    thus the carrier of H = MSAEnd U1;
    thus the multF of H = MSAEndComp U1;
    thus thesis;
  end;
  uniqueness;
end;

registration
  let S, U1;
  cluster MSAEndMonoid U1 -> non empty;
  coherence
  proof
    reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7;
    set H = multLoopStr(#MSAEnd U1, MSAEndComp U1, i#);
    1.H = i;
    hence thesis by Def6;
  end;
end;

Lm2: now
  let S,U1;
  set F = MSAEndMonoid U1;
  let x, e be Element of F;
  reconsider i = e, y = x as Element of MSAEnd U1 by Def6;
  assume
A1: e = id the Sorts of U1;
  thus x*e = (MSAEndComp U1).(y,i) by Def6
    .= i**y by Def5
    .= x by A1,MSUALG_3:4;
  thus e*x = (MSAEndComp U1).(i,y) by Def6
    .= y**i by Def5
    .= x by A1,MSUALG_3:3;
end;

registration
  let S,U1;
  cluster MSAEndMonoid U1 -> well-unital associative;
  coherence
  proof
    reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7;
    set H = multLoopStr(#MSAEnd U1, MSAEndComp U1, i#);
    thus MSAEndMonoid U1 is well-unital
    proof
      let x be Element of MSAEndMonoid U1;
      1.MSAEndMonoid U1 = i by Def6;
      hence thesis by Lm2;
    end;
    for f, g, h be Element of H holds (f * g) * h = f * (g * h)
    proof
      let f, g, h be Element of H;
      reconsider A = f, B = g, C = h as Element of MSAEnd U1;
A1:   g * h = C ** B by Def5;
      f * g = B ** A by Def5;
      hence (f * g) * h = C ** (B ** A) by Def5
        .= (C ** B) ** A by PBOOLE:140
        .= f * (g * h) by A1,Def5;
    end;
    then 1.H = i & H is associative by GROUP_1:def 3;
    hence thesis by Def6;
  end;
end;

theorem Th10:
  for x, y be Element of MSAEndMonoid U1 for f, g be Element of
  MSAEnd U1 st x = f & y = g holds x * y = g ** f
proof
  reconsider i = id the Sorts of U1 as Element of MSAEnd U1 by Th7;
  let x, y be Element of MSAEndMonoid U1;
  let f, g be Element of MSAEnd U1;
  set H = multLoopStr(# MSAEnd U1, MSAEndComp U1, i #);
  1.H = i;
  then
A1: MSAEndMonoid U1 = H by Def6;
  assume x = f & y = g;
  hence thesis by A1,Def5;
end;

theorem
  id the Sorts of U1 = 1_MSAEndMonoid U1 by Def6;

theorem Th12:
  for f be Element of UAEnd UA holds 0 .--> f is
  ManySortedFunction of MSAlg UA, MSAlg UA
proof
  let f be Element of UAEnd UA;
  MSAlg f is ManySortedFunction of MSAlg UA, MSAlg UA by MSUHOM_1:9;
  hence thesis by MSUHOM_1:def 3;
end;

Lm3: for h be Function st (dom h = UAEnd UA & for x be set st x in UAEnd UA
holds h.x = 0 .--> x) holds rng h = MSAEnd (MSAlg UA)
proof
  let h be Function such that
A1: dom h = UAEnd UA and
A2: for x be set st x in UAEnd UA holds h.x = 0 .--> x;
A3: MSAEnd (MSAlg UA) c= rng h
  proof
    let x be set;
    assume
A4: x in MSAEnd (MSAlg UA);
    then reconsider f = x as ManySortedFunction of MSAlg UA, MSAlg UA by Def4;
    the carrier of MSSign UA = {0} by MSUALG_1:def 8;
    then
A5: f = 0 .--> f.0 by AUTALG_1:11;
A6: f is_homomorphism MSAlg UA, MSAlg UA by A4,Def4;
    ex q be set st q in dom h & x = h.q
    proof
      take q = f.0;
      f is ManySortedFunction of MSAlg UA, (MSAlg UA Over MSSign UA) by
MSUHOM_1:9;
      then reconsider q9 = q as Function of UA, UA by AUTALG_1:31;
      MSAlg q9 = f by A5,MSUHOM_1:def 3;
      then
      MSAlg q9 is_homomorphism MSAlg UA, (MSAlg UA Over MSSign UA) by A6,
MSUHOM_1:9;
      then q9 is_homomorphism UA, UA by MSUHOM_1:21;
      hence q in dom h by A1,Def1;
      hence thesis by A1,A2,A5;
    end;
    hence thesis by FUNCT_1:def 3;
  end;
  rng h c= MSAEnd (MSAlg UA)
  proof
    let x be set;
    assume x in rng h;
    then consider q be set such that
A7: q in dom h and
A8: x = h.q by FUNCT_1:def 3;
    consider q9 be Element of UAEnd UA such that
A9: q9 = q by A1,A7;
    x = 0 .--> q & 0 .--> q is ManySortedFunction of MSAlg UA, MSAlg UA by A1
,A2,A7,A8,Th12;
    then consider d be ManySortedFunction of MSAlg UA, MSAlg UA such that
A10: d = x;
    q9 is_homomorphism UA, UA by Def1;
    then
A11: MSAlg q9 is_homomorphism MSAlg UA, MSAlg UA Over MSSign UA by MSUHOM_1:16;
    MSAlg q9 = 0 .--> q by A9,MSUHOM_1:def 3
      .= x by A1,A2,A7,A8;
    then d is_homomorphism MSAlg UA, MSAlg UA by A10,A11,MSUHOM_1:9;
    hence thesis by A10,Def4;
  end;
  hence rng h = MSAEnd (MSAlg UA) by A3,XBOOLE_0:def 10;
end;

registration
  cluster left_unital for non empty multLoopStr;
  existence
  proof
    set m = the BinOp of {0},u = the Element of {0};
    take multLoopStr(#{0},m,u#);
    let x be Element of multLoopStr(#{0},m,u#);
    thus (1.multLoopStr(#{0},m,u#))*x = 0 by TARSKI:def 1
      .= x by TARSKI:def 1;
  end;
end;

registration
  let G,H be well-unital non empty multLoopStr;
  cluster multiplicative unity-preserving for Function of G,H;
  existence
  proof
    reconsider m = (the carrier of G) --> 1.H as Function of the carrier of G,
    the carrier of H;
    reconsider m as Function of G,H;
    take m;
    for x,y being Element of G holds m.(x*y) = (m.x)*(m.y)
    proof
      let x,y be Element of G;
      m.(x*y) = 1.H by FUNCOP_1:7
        .= 1.H * 1.H by VECTSP_1:def 8
        .= (m.x)* 1.H by FUNCOP_1:7
        .= (m.x)*(m.y) by FUNCOP_1:7;
      hence thesis;
    end;
    hence m is multiplicative by GROUP_6:def 6;
    thus m.1_G = 1_H by FUNCOP_1:7;
  end;
end;

definition
  let G,H be well-unital non empty multLoopStr;
  mode Homomorphism of G,H is multiplicative unity-preserving Function of G,H;
end;

theorem Th13:
  for G be well-unital non empty multLoopStr holds id the
  carrier of G is Homomorphism of G,G
proof
  let G be well-unital non empty multLoopStr;
  reconsider f = id the carrier of G as Function of G,G;
A1: for a,b be Element of G holds f.(a * b) = f.a * f.b
  proof
    let a,b be Element of G;
    f.(a * b) = a * b by FUNCT_1:18
      .= f.a * b by FUNCT_1:18
      .= f.a * f.b by FUNCT_1:18;
    hence thesis;
  end;
  f.1_G = 1_G by FUNCT_1:18;
  hence thesis by A1,GROUP_1:def 13,GROUP_6:def 6;
end;

definition
  let G,H be well-unital non empty multLoopStr;

  pred G,H are_isomorphic means
  :Def7:
  ex h be Homomorphism of G,H st h is bijective;
  reflexivity
  proof
    let G be well-unital non empty multLoopStr;
    reconsider i = id the carrier of G as Homomorphism of G,G by Th13;
A1: the carrier of G c= rng i
    proof
      let y be set;
      assume
A2:   y in the carrier of G;
      ex x being set st x in dom i & y = i.x
      proof
        take y;
        thus thesis by A2,FUNCT_1:17;
      end;
      hence thesis by FUNCT_1:def 3;
    end;
    rng i c= the carrier of G by RELAT_1:def 19;
    then rng i = the carrier of G by A1,XBOOLE_0:def 10;
    then i is onto by FUNCT_2:def 3;
    hence thesis;
  end;
end;

theorem Th14:
  for h be Function st (dom h = UAEnd UA & for x be set st x in
  UAEnd UA holds h.x = 0 .--> x) holds h is Homomorphism of UAEndMonoid UA,
  MSAEndMonoid (MSAlg UA)
proof
  reconsider i = id the Sorts of MSAlg UA as Element of MSAEnd MSAlg UA by Th7
;
  set G = UAEndMonoid UA;
  set H = MSAEndMonoid (MSAlg UA), M = multLoopStr (# MSAEnd MSAlg UA,
    MSAEndComp MSAlg UA,i #);
  reconsider e = id the carrier of UA as Element of UAEnd UA by Th2;
  let h be Function such that
A1: dom h = UAEnd UA and
A2: for x be set st x in UAEnd UA holds h.x = 0 .--> x;
A3: the carrier of G = dom h by A1,Def3;
  1.M = i;
  then
A4: H = M by Def6;
  then rng h c= the carrier of H by A1,A2,Lm3;
  then reconsider h9 = h as Function of G,H by A3,FUNCT_2:def 1,RELSET_1:4;
A5: h9.(e) = 0 .--> (e) by A2;
A6: for a,b being Element of G holds h9.(a * b) = h9.a * h9.b
  proof
    let a, b be Element of UAEndMonoid UA;
    reconsider a9 = a, b9 = b as Element of UAEnd UA by Def3;
    reconsider A = 0 .--> a9, B = 0 .--> b9 as ManySortedFunction of MSAlg UA,
    MSAlg UA by Th12;
    reconsider ha = h9.a, hb = h9.b as Element of MSAEnd MSAlg UA by Def6;
A7: h9.(b9 * a9) = 0 .--> (b9 * a9) by A2,Th3;
    reconsider A9 = A, B9 = B as Element of MSAEndMonoid MSAlg UA by A4,Th9;
A8: ha = A9 & hb = B9 by A2;
    thus h9.(a * b) = h9.(b9 * a9) by Th4
      .= MSAlg (b9 * a9) by A7,MSUHOM_1:def 3
      .= (MSAlg b9) ** (MSAlg a9) by MSUHOM_1:26
      .= B ** MSAlg a9 by MSUHOM_1:def 3
      .= B ** A by MSUHOM_1:def 3
      .= h9.a * h9.b by A8,Th10;
  end;
  h9.1.G = h9.e by Def3
    .= MSAlg (e) by A5,MSUHOM_1:def 3
    .= i by MSUHOM_1:25
    .= 1_H by Def6;
  then h9.1_G = 1_H;
  hence thesis by A6,GROUP_1:def 13,GROUP_6:def 6;
end;

theorem Th15:
  for h be Homomorphism of UAEndMonoid UA, MSAEndMonoid (MSAlg UA)
  st for x be set st x in UAEnd UA holds h.x = 0 .--> x holds h is bijective
proof
  reconsider e = id the Sorts of MSAlg UA as Element of MSAEnd MSAlg UA by Th7
;
  set N = multLoopStr (# MSAEnd MSAlg UA, MSAEndComp MSAlg UA,e#);
  reconsider i = id the carrier of UA as Element of UAEnd UA by Th2;
  let h be Homomorphism of UAEndMonoid UA, MSAEndMonoid (MSAlg UA);
  set G = UAEndMonoid UA;
  set H = MSAEndMonoid MSAlg UA, M = multLoopStr (# UAEnd UA, UAEndComp UA,i#);
  1.M = i;
  then
A1: G = M by Def3;
  assume
A2: for x be set st x in UAEnd UA holds h.x = 0 .--> x;
  for a, b be Element of G st h.a = h.b holds a = b
  proof
    let a, b be Element of G;
    assume
A3: h.a = h.b;
A4: h.b = 0 .--> b by A2,A1
      .= [:{0}, {b}:];
    h.a = 0 .--> a by A2,A1
      .= [:{0}, {a}:];
    then {a} = {b} by A3,A4,ZFMISC_1:110;
    hence thesis by ZFMISC_1:3;
  end;
  then
A5: h is one-to-one by GROUP_6:1;
  1.N = e;
  then
A6: H = N by Def6;
  dom h = UAEnd UA by A1,FUNCT_2:def 1;
  then rng h = the carrier of MSAEndMonoid (MSAlg UA) by A2,A6,Lm3;
  then h is onto by FUNCT_2:def 3;
  hence h is bijective by A5;
end;

theorem
  UAEndMonoid UA, MSAEndMonoid (MSAlg UA) are_isomorphic
proof
  set G = UAEndMonoid UA;
  set H = MSAEndMonoid (MSAlg UA);
  ex h be Homomorphism of G,H st h is bijective
  proof
    deffunc F(set) = 0 .--> $1;
    consider h be Function such that
A1: dom h = UAEnd UA & for x be set st x in UAEnd UA holds h.x = F(x)
    from FUNCT_1:sch 3;
    reconsider h as Homomorphism of G, H by A1,Th14;
    h is bijective by A1,Th15;
    hence thesis;
  end;
  hence thesis by Def7;
end;