endalg.miz



    begin

    reserve UA for Universal_Algebra;

    definition

      let UA;

      :: ENDALG:def1

      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 ;

      existence

      proof

        set F = { x where x be Element of ( Funcs (the carrier of UA,the carrier of UA)) : x is_homomorphism };

        

         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 by ALG_1: 5, FUNCT_2: 8;

          hence thesis;

        end;

        F is functional

        proof

          let q be object;

          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 ;

          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 ;

          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

        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 ;

          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 ;

        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 and

         A4: for h be Function of UA, UA holds h in F2 iff h is_homomorphism ;

        

         A5: for f be Element of F2 holds f is Function of UA, UA;

        

         A6: F2 c= F1

        proof

          let q be object;

          assume

           A7: q in F2;

          then

          reconsider h1 = q as Function of UA, UA by A5;

          h1 is_homomorphism 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 object;

          assume

           A9: q in F1;

          then

          reconsider h1 = q as Function of UA, UA by A8;

          h1 is_homomorphism by A3, A9;

          hence thesis by A4;

        end;

        hence thesis by A6, XBOOLE_0:def 10;

      end;

    end

    theorem :: ENDALG:1

    ( UAEnd UA) c= ( Funcs (the carrier of UA,the carrier of UA))

    proof

      let q be object;

      assume q in ( UAEnd UA);

      then q is Element of ( UAEnd UA);

      hence thesis by FUNCT_2: 9;

    end;

    theorem :: ENDALG:2

    

     Th2: ( id the carrier of UA) in ( UAEnd UA)

    proof

      ( id the carrier of UA) is_homomorphism by ALG_1: 5;

      hence thesis by Def1;

    end;

    theorem :: ENDALG:3

    

     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 & f2 is_homomorphism by Def1;

      then (f1 * f2) is_homomorphism by ALG_1: 6;

      hence thesis by Def1;

    end;

    definition

      let UA;

      :: ENDALG:def2

      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) holds 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 be 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;

      :: ENDALG:def3

      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;

        hence thesis by Def3;

      end;

    end

    theorem :: ENDALG:4

    

     Th4: for x,y be Element of ( UAEndMonoid UA) holds 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 :: ENDALG:5

    ( 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;

      :: ENDALG:def4

      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[ object] 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 object 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 be 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)) by A1;

        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

         A2: for f be Element of F1 holds f is ManySortedFunction of U1, U1 and

         A3: for h be ManySortedFunction of U1, U1 holds h in F1 iff h is_homomorphism (U1,U1) and

         A4: for f be Element of F2 holds f is ManySortedFunction of U1, U1 and

         A5: for h be ManySortedFunction of U1, U1 holds h in F2 iff h is_homomorphism (U1,U1);

        

         A6: F2 c= F1

        proof

          let q be object;

          assume

           A7: q in F2;

          then

          reconsider h1 = q as ManySortedFunction of U1, U1 by A4;

          h1 is_homomorphism (U1,U1) by A5, A7;

          hence thesis by A3;

        end;

        F1 c= F2

        proof

          let q be object;

          assume

           A8: q in F1;

          then

          reconsider h1 = q as ManySortedFunction of U1, U1 by A2;

          h1 is_homomorphism (U1,U1) by A3, A8;

          hence thesis by A5;

        end;

        hence thesis by A6, XBOOLE_0:def 10;

      end;

    end

    theorem :: ENDALG:6

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

    theorem :: ENDALG:7

    

     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 :: ENDALG:8

    

     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 :: ENDALG:9

    

     Th9: for F be ManySortedFunction of ( MSAlg UA), ( MSAlg UA) holds 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 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;

      :: ENDALG:def5

      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) holds 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 be 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;

      :: ENDALG:def6

      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;

        hence thesis by Def6;

      end;

    end

    theorem :: ENDALG:10

    

     Th10: for x,y be Element of ( MSAEndMonoid U1) holds 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 :: ENDALG:11

    ( id the Sorts of U1) = ( 1_ ( MSAEndMonoid U1)) by Def6;

    theorem :: ENDALG:12

    

     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 object 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 object st x in ( UAEnd UA) holds (h . x) = ( 0 .--> x);

      

       A3: ( MSAEnd ( MSAlg UA)) c= ( rng h)

      proof

        let x be object;

        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 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 object;

        assume x in ( rng h);

        then

        consider q be object 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 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 be 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))

          .= ((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 :: ENDALG:13

    

     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));

      (f . ( 1_ G)) = ( 1_ G);

      hence thesis by A1, GROUP_1:def 13, GROUP_6:def 6;

    end;

    definition

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

      :: ENDALG:def7

      pred G,H are_isomorphic means 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 object;

          assume

           A2: y in the carrier of G;

          ex x be 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;

        hence thesis;

      end;

    end

    theorem :: ENDALG:14

    

     Th14: for h be Function st (( dom h) = ( UAEnd UA) & for x be object 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 object 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 be 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 :: ENDALG:15

    

     Th15: for h be Homomorphism of ( UAEndMonoid UA), ( MSAEndMonoid ( MSAlg UA)) st for x be object 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 object 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;

      hence h is bijective by A5;

    end;

    theorem :: ENDALG:16

    (( 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( object) = ( 0 .--> $1);

        consider h be Function such that

         A1: ( dom h) = ( UAEnd UA) & for x be object 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;

    end;