autalg_1.miz

    begin

    reserve UA for Universal_Algebra,

f,g for Function of UA, UA;

    theorem :: AUTALG_1:1



     Th1: ( id the carrier of UA) is_isomorphism

    proof

      set I = ( id the carrier of UA);

      I is_homomorphism by ALG_1: 5;

      hence I is_monomorphism ;

      I is_homomorphism & ( rng I) = the carrier of UA by ALG_1: 5, RELAT_1: 45;

      hence I is_epimorphism ;

    end;

    definition

      let UA;

      :: AUTALG_1:def1

      func UAAut 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_isomorphism ;

      existence

      proof

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



         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_isomorphism by Th1, FUNCT_2: 8;

          hence thesis;

        end;

        reconsider F as set;

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

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

          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_isomorphism

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

          hence thesis;

        end;



         A2: h is Element of ( Funcs (the carrier of UA,the carrier of UA)) by FUNCT_2: 8;

        assume h is_isomorphism ;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let F1,F2 be FUNCTION_DOMAIN of the carrier of UA, the carrier of UA such that

         A3: for h be Function of UA, UA holds h in F1 iff h is_isomorphism and

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



         A5: F2 c= F1

        proof

          let q be object;

          assume

           A6: q in F2;

          then

          reconsider h1 = q as Function of UA, UA by FUNCT_2:def 12;

          h1 is_isomorphism by A4, A6;

          hence thesis by A3;

        end;

        F1 c= F2

        proof

          let q be object;

          assume

           A7: q in F1;

          then

          reconsider h1 = q as Function of UA, UA by FUNCT_2:def 12;

          h1 is_isomorphism by A3, A7;

          hence thesis by A4;

        end;

        hence thesis by A5;

      end;

    end

    theorem :: AUTALG_1:2

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

    proof

      let q be object;

      assume q in ( UAAut UA);

      then ex f be Element of ( UAAut UA) st f = q;

      hence thesis by FUNCT_2: 9;

    end;

    theorem :: AUTALG_1:3



     Th3: ( id the carrier of UA) in ( UAAut UA)

    proof

      ( id the carrier of UA) is_isomorphism by Th1;

      hence thesis by Def1;

    end;

    theorem :: AUTALG_1:4

    for f, g st f is Element of ( UAAut UA) & g = (f " ) holds g is_isomorphism

    proof

      let f, g;

      assume that

       A1: f is Element of ( UAAut UA) and

       A2: g = (f " );

      f is_isomorphism by A1, Def1;

      hence thesis by A2, ALG_1: 10;

    end;



     Lm1: for f st f is_isomorphism holds (f " ) is Function of UA, UA

    proof

      let f;

      assume

       A1: f is_isomorphism ;

      then f is_epimorphism ;

      then

       A2: ( rng f) = the carrier of UA;

      f is one-to-one by A1, ALG_1: 7;

      hence thesis by A2, FUNCT_2: 25;

    end;

    theorem :: AUTALG_1:5



     Th5: for f be Element of ( UAAut UA) holds (f " ) in ( UAAut UA)

    proof

      let f be Element of ( UAAut UA);



       A1: f is_isomorphism by Def1;

      then (f " ) is Function of UA, UA by Lm1;

      then

      consider ff be Function of UA, UA such that

       A2: ff = (f " );

      ff is_isomorphism by A1, A2, ALG_1: 10;

      hence thesis by A2, Def1;

    end;

    theorem :: AUTALG_1:6



     Th6: for f1,f2 be Element of ( UAAut UA) holds (f1 * f2) in ( UAAut UA)

    proof

      let f1,f2 be Element of ( UAAut UA);

      f1 is_isomorphism & f2 is_isomorphism by Def1;

      then (f1 * f2) is_isomorphism by ALG_1: 11;

      hence thesis by Def1;

    end;

    definition

      let UA;

      :: AUTALG_1:def2

      func UAAutComp UA -> BinOp of ( UAAut UA) means

      : Def2: for x,y be Element of ( UAAut UA) holds (it . (x,y)) = (y * x);

      existence

      proof

        defpred P[ Element of ( UAAut UA), Element of ( UAAut UA), set] means $3 = ($2 * $1);



         A1: for x,y be Element of ( UAAut UA) holds ex m be Element of ( UAAut UA) st P[x, y, m]

        proof

          let x,y be Element of ( UAAut UA);

          reconsider xx = x, yy = y as Function of UA, UA;

          reconsider m = (yy * xx) as Element of ( UAAut UA) by Th6;

          take m;

          thus thesis;

        end;

        thus ex IT be BinOp of ( UAAut UA) st for x,y be Element of ( UAAut UA) holds P[x, y, (IT . (x,y))] from BINOP_1:sch 3( A1);

      end;

      uniqueness

      proof

        let b1,b2 be BinOp of ( UAAut UA) such that

         A2: for x,y be Element of ( UAAut UA) holds (b1 . (x,y)) = (y * x) and

         A3: for x,y be Element of ( UAAut UA) holds (b2 . (x,y)) = (y * x);

        for x,y be Element of ( UAAut UA) holds (b1 . (x,y)) = (b2 . (x,y))

        proof

          let x,y be Element of ( UAAut 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;

      :: AUTALG_1:def3

      func UAAutGroup UA -> Group equals multMagma (# ( UAAut UA), ( UAAutComp UA) #);

      coherence

      proof

        set H = multMagma (# ( UAAut UA), ( UAAutComp UA) #);



         A1: ex e be Element of H st for h be Element of H holds (h * e) = h & (e * h) = h & ex g be Element of H st (h * g) = e & (g * h) = e

        proof

          reconsider e = ( id the carrier of UA) as Element of H by Th3;

          take e;

          let h be Element of H;

          consider A be Element of ( UAAut UA) such that

           A2: A = h;

          (h * e) = (( id the carrier of UA) * A) by A2, Def2

          .= A by FUNCT_2: 17;

          hence (h * e) = h by A2;

          (e * h) = (A * ( id the carrier of UA)) by A2, Def2

          .= A by FUNCT_2: 17;

          hence (e * h) = h by A2;

          reconsider g = (A " ) as Element of H by Th5;

          take g;



           A3: A is_isomorphism by Def1;

          then

           A4: A is one-to-one by ALG_1: 7;

          A is_epimorphism by A3;

          then

           A5: ( rng A) = the carrier of UA;



          thus (h * g) = ((A " ) * A) by A2, Def2

          .= e by A4, A5, FUNCT_2: 29;



          thus (g * h) = (A * (A " )) by A2, Def2

          .= e by A4, A5, FUNCT_2: 29;

        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 ( UAAut UA);



           A6: (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 A6, Def2;

        end;

        hence thesis by A1, GROUP_1:def 2, GROUP_1:def 3;

      end;

    end

    registration

      let UA;

      cluster ( UAAutGroup UA) -> strict;

      coherence ;

    end



     Lm2: for f be Element of ( UAAut UA) holds ( dom f) = ( rng f) & ( dom f) = the carrier of UA

    proof

      let f be Element of ( UAAut UA);



       A1: f is_isomorphism by Def1;

      then ( dom f) = the carrier of UA by ALG_1: 8;

      hence thesis by A1, ALG_1: 8;

    end;

    theorem :: AUTALG_1:7

    for x,y be Element of ( UAAutGroup UA) holds for f,g be Element of ( UAAut UA) st x = f & y = g holds (x * y) = (g * f) by Def2;

    theorem :: AUTALG_1:8



     Th8: ( id the carrier of UA) = ( 1_ ( UAAutGroup UA))

    proof

      set f = the Element of ( UAAutGroup UA);

      reconsider g = ( id the carrier of UA) as Element of ( UAAutGroup UA) by Th3;

      consider g1 be Function of the carrier of UA, the carrier of UA such that

       A1: g1 = g;

      f is Element of ( UAAut UA);

      then

      consider f1 be Function of the carrier of UA, the carrier of UA such that

       A2: f1 = f;

      (g * f) = (f1 * g1) by A1, A2, Def2

      .= f by A1, A2, FUNCT_2: 17;

      hence thesis by GROUP_1: 7;

    end;

    theorem :: AUTALG_1:9

    for f be Element of ( UAAut UA) holds for g be Element of ( UAAutGroup UA) st f = g holds (f " ) = (g " )

    proof

      let f be Element of ( UAAut UA);

      let g be Element of ( UAAutGroup UA);

      consider g1 be Element of ( UAAut UA) such that

       A1: g1 = (g " );

      assume f = g;

      then (g1 * f) = (g * (g " )) by A1, Def2;

      then (g1 * f) = ( 1_ ( UAAutGroup UA)) by GROUP_1:def 5;

      then

       A2: (g1 * f) = ( id the carrier of UA) by Th8;

      f is_isomorphism by Def1;

      then f is_monomorphism ;

      then

       A3: f is one-to-one;

      ( rng f) = ( dom f) by Lm2

      .= the carrier of UA by Lm2;

      hence thesis by A1, A3, A2, FUNCT_2: 30;

    end;

    begin

    reserve I for set,

A,B,C for ManySortedSet of I;

    theorem :: AUTALG_1:10

    A is_transformable_to B & B is_transformable_to C implies A is_transformable_to C

    proof

      assume that

       A1: A is_transformable_to B and

       A2: B is_transformable_to C;

      let i be set;

      assume

       A3: i in I;

      then (B . i) = {} implies (A . i) = {} by A1;

      hence thesis by A2, A3;

    end;

    theorem :: AUTALG_1:11



     Th11: for x be set, A be ManySortedSet of {x} holds A = (x .--> (A . x))

    proof

      let x be set;

      let A be ManySortedSet of {x};



       A1: ( dom A) = {x} by PARTFUN1:def 2;

      then ( rng A) = {(A . x)} by FUNCT_1: 4;

      hence thesis by A1, FUNCOP_1: 9;

    end;

    theorem :: AUTALG_1:12



     Th12: for A,B be non-empty ManySortedSet of I holds for F be ManySortedFunction of A, B st F is "1-1" "onto" holds (F "" ) is "1-1" "onto"

    proof

      let A,B be non-empty ManySortedSet of I;

      let F be ManySortedFunction of A, B;

      assume

       A1: F is "1-1" "onto";

      now

        let i be set;

        assume

         A2: i in I;

        then

        reconsider g = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;

        g is one-to-one by A1, A2, MSUALG_3: 1;

        then (g " ) is one-to-one;

        hence ((F "" ) . i) is one-to-one by A1, A2, MSUALG_3:def 4;

      end;

      hence (F "" ) is "1-1" by MSUALG_3: 1;

      thus (F "" ) is "onto"

      proof

        let i be set;

        assume

         A3: i in I;

        then

        reconsider g = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;



         A4: g is one-to-one by A1, A3, MSUALG_3: 1;

        (A . i) = ( dom g) by A3, FUNCT_2:def 1

        .= ( rng (g " )) by A4, FUNCT_1: 33;

        hence thesis by A1, A3, MSUALG_3:def 4;

      end;

    end;

    theorem :: AUTALG_1:13

    for A,B be non-empty ManySortedSet of I holds for F be ManySortedFunction of A, B st F is "1-1" "onto" holds ((F "" ) "" ) = F

    proof

      let A,B be non-empty ManySortedSet of I;

      let F be ManySortedFunction of A, B;

      assume

       A1: F is "1-1" "onto";

      now

        let i be object;

        assume

         A2: i in I;

        then

        reconsider f = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;

        reconsider f9 = ((F "" ) . i) as Function of (B . i), (A . i) by A2, PBOOLE:def 15;

        f is one-to-one by A1, A2, MSUALG_3: 1;

        then

         A3: ((f " ) " ) = f by FUNCT_1: 43;

        (F "" ) is "1-1" "onto" by A1, Th12;

        then (((F "" ) "" ) . i) = (f9 " ) by A2, MSUALG_3:def 4;

        hence (((F "" ) "" ) . i) = (F . i) by A1, A2, A3, MSUALG_3:def 4;

      end;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: AUTALG_1:14



     Th14: for F,G be Function-yielding Function st F is "1-1" & G is "1-1" holds (G ** F) is "1-1"

    proof

      let F,G be Function-yielding Function such that

       A1: F is "1-1" and

       A2: G is "1-1";

      let i be set, f be Function such that

       A3: i in ( dom (G ** F)) and

       A4: ((G ** F) . i) = f;



       A5: ( dom (G ** F)) = (( dom G) /\ ( dom F)) by PBOOLE:def 19;

      then i in ( dom F) by A3, XBOOLE_0:def 4;

      then

       A6: (F . i) is one-to-one by A1;

      i in ( dom G) by A3, A5, XBOOLE_0:def 4;

      then (G . i) is one-to-one by A2;

      then ((G . i) * (F . i)) is one-to-one by A6;

      hence thesis by A3, A4, PBOOLE:def 19;

    end;

    theorem :: AUTALG_1:15



     Th15: for B,C be non-empty ManySortedSet of I holds for F be ManySortedFunction of A, B holds for G be ManySortedFunction of B, C st F is "onto" & G is "onto" holds (G ** F) is "onto"

    proof

      let B,C be non-empty ManySortedSet of I;

      let F be ManySortedFunction of A, B;

      let G be ManySortedFunction of B, C;

      assume

       A1: F is "onto" & G is "onto";

      now

        let i be set;

        assume

         A2: i in I;

        then

        reconsider f = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;

        reconsider g = (G . i) as Function of (B . i), (C . i) by A2, PBOOLE:def 15;

        ( rng f) = (B . i) & ( rng g) = (C . i) by A1, A2;

        then ( rng (g * f)) = (C . i) by A2, FUNCT_2: 14;

        hence ( rng ((G ** F) . i)) = (C . i) by A2, MSUALG_3: 2;

      end;

      hence thesis;

    end;

    theorem :: AUTALG_1:16

    for A,B,C be non-empty ManySortedSet of I holds for F be ManySortedFunction of A, B holds for G be ManySortedFunction of B, C st F is "1-1" "onto" & G is "1-1" "onto" holds ((G ** F) "" ) = ((F "" ) ** (G "" ))

    proof

      let A,B,C be non-empty ManySortedSet of I;

      let F be ManySortedFunction of A, B;

      let G be ManySortedFunction of B, C;

      assume that

       A1: F is "1-1" "onto" and

       A2: G is "1-1" "onto";

      now

        let i be object;

        assume

         A3: i in I;

        then

        reconsider f = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;



         A4: f is one-to-one by A1, A3, MSUALG_3: 1;

        reconsider g = (G . i) as Function of (B . i), (C . i) by A3, PBOOLE:def 15;



         A5: g is one-to-one by A2, A3, MSUALG_3: 1;

        ((F "" ) . i) = (f " ) & ( rng f) = (B . i) by A1, A3, MSUALG_3:def 4;

        then

        reconsider ff = ((F "" ) . i) as Function of (B . i), (A . i) by A4, FUNCT_2: 25;



         A6: (G ** F) is "1-1" "onto" by A1, A2, Th14, Th15;

        ((G ** F) . i) = (g * f) by A3, MSUALG_3: 2;

        then

         A7: (((G ** F) "" ) . i) = ((g * f) " ) by A3, A6, MSUALG_3:def 4;

        ((G "" ) . i) = (g " ) & ( rng g) = (C . i) by A2, A3, MSUALG_3:def 4;

        then

        reconsider gg = ((G "" ) . i) as Function of (C . i), (B . i) by A5, FUNCT_2: 25;

        (((F "" ) ** (G "" )) . i) = (ff * gg) by A3, MSUALG_3: 2

        .= (ff * (g " )) by A2, A3, MSUALG_3:def 4

        .= ((f " ) * (g " )) by A1, A3, MSUALG_3:def 4;

        hence (((G ** F) "" ) . i) = (((F "" ) ** (G "" )) . i) by A4, A5, A7, FUNCT_1: 44;

      end;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: AUTALG_1:17



     Th17: for A,B be non-empty ManySortedSet of I holds for F be ManySortedFunction of A, B holds for G be ManySortedFunction of B, A st F is "1-1" & F is "onto" & (G ** F) = ( id A) holds G = (F "" )

    proof

      let A,B be non-empty ManySortedSet of I;

      let F be ManySortedFunction of A, B;

      let G be ManySortedFunction of B, A;

      assume that

       A1: F is "1-1" and

       A2: F is "onto" and

       A3: (G ** F) = ( id A);

      now

        let i be object;

        assume

         A4: i in I;

        then

        reconsider f = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;



         A5: f is one-to-one by A1, A4, MSUALG_3: 1;

        reconsider g = (G . i) as Function of (B . i), (A . i) by A4, PBOOLE:def 15;

        ((G ** F) . i) = ( id (A . i)) by A3, A4, MSUALG_3:def 1;

        then

         A6: (g * f) = ( id (A . i)) by A4, MSUALG_3: 2;

        ((F "" ) . i) = (f " ) & ( rng f) = (B . i) by A1, A2, A4, MSUALG_3:def 4;

        hence (G . i) = ((F "" ) . i) by A4, A6, A5, FUNCT_2: 30;

      end;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: AUTALG_1:18



     Th18: A is_transformable_to B implies ( (Funcs) (A,B)) is non-empty

    proof

      assume

       A1: A is_transformable_to B;



       A2: for i be set st i in I holds ( Funcs ((A . i),(B . i))) <> {}

      proof

        let i be set;

        assume i in I;

        then (B . i) = {} implies (A . i) = {} by A1;

        hence thesis by FUNCT_2: 8;

      end;

      for i be object st i in I holds (( (Funcs) (A,B)) . i) <> {}

      proof

        let i be object;

        assume

         A3: i in I;

        then (( (Funcs) (A,B)) . i) = ( Funcs ((A . i),(B . i))) by PBOOLE:def 17;

        hence thesis by A2, A3;

      end;

      then for i be object st i in I holds (( (Funcs) (A,B)) . i) is non empty;

      hence thesis by PBOOLE:def 13;

    end;

    definition

      let I, A, B;

      assume

       A1: A is_transformable_to B;

      :: AUTALG_1:def4

      func MSFuncs (A,B) -> non empty set equals

      : Def4: ( product ( (Funcs) (A,B)));

      coherence

      proof

        ( (Funcs) (A,B)) is non-empty by A1, Th18;

        then not {} in ( rng ( (Funcs) (A,B))) by PBOOLE: 137;

        hence thesis by CARD_3: 26;

      end;

    end

    theorem :: AUTALG_1:19



     Th19: A is_transformable_to B implies for x be set st x in ( MSFuncs (A,B)) holds x is ManySortedFunction of A, B

    proof

      assume

       A1: A is_transformable_to B;

      set f = ( (Funcs) (A,B));

      let x be set;

      assume x in ( MSFuncs (A,B));

      then x in ( product f) by A1, Def4;

      then

      consider g be Function such that

       A2: x = g and

       A3: ( dom g) = ( dom f) and

       A4: for i be object st i in ( dom f) holds (g . i) in (f . i) by CARD_3:def 5;



       A5: ( dom f) = I by PARTFUN1:def 2;



       A6: for i be set st i in I holds (g . i) in ( Funcs ((A . i),(B . i)))

      proof

        let i be set;

        assume

         A7: i in I;

        then (( (Funcs) (A,B)) . i) = ( Funcs ((A . i),(B . i))) by PBOOLE:def 17;

        hence thesis by A4, A5, A7;

      end;



       A8: for i be set st i in I holds ex F be Function st F = (g . i) & ( dom F) = (A . i) & ( rng F) c= (B . i)

      proof

        let i be set;

        assume i in I;

        then (g . i) in ( Funcs ((A . i),(B . i))) by A6;

        hence thesis by FUNCT_2:def 2;

      end;



       A9: for i be object st i in I holds (g . i) is Function of (A . i), (B . i)

      proof

        let i be object;

        assume

         A10: i in I;

        ex F be Function st F = (g . i) & ( dom F) = (A . i) & ( rng F) c= (B . i) by A8, A10;

        hence thesis by FUNCT_2: 2;

      end;

      ( dom g) = I by A3, PARTFUN1:def 2;

      then g is ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      hence thesis by A2, A9, PBOOLE:def 15;

    end;

    theorem :: AUTALG_1:20



     Th20: A is_transformable_to B implies for g be ManySortedFunction of A, B holds g in ( MSFuncs (A,B))

    proof

      assume

       A1: A is_transformable_to B;

      set f = ( (Funcs) (A,B));

      let g be ManySortedFunction of A, B;



       A2: ( dom f) = I by PARTFUN1:def 2;

       A3:

      now

        let x be object;

        assume

         A4: x in ( dom f);

        then

        reconsider i = x as Element of I by PARTFUN1:def 2;



         A5: (g . i) is Function of (A . i), (B . i) by A2, A4, PBOOLE:def 15;

        (B . i) = {} implies (A . i) = {} by A1, A2, A4;

        then (g . i) in ( Funcs ((A . i),(B . i))) by A5, FUNCT_2: 8;

        hence (g . x) in (f . x) by A2, A4, PBOOLE:def 17;

      end;

      ( dom g) = I by PARTFUN1:def 2;

      then g in ( product f) by A2, A3, CARD_3: 9;

      hence thesis by A1, Def4;

    end;

    registration

      let I, A;

      cluster ( (Funcs) (A,A)) -> non-empty;

      coherence

      proof

        for i be object st i in I holds (( (Funcs) (A,A)) . i) is non empty

        proof

          let i be object;

          assume

           A1: i in I;

          then (( id A) . i) is Function of (A . i), (A . i) by PBOOLE:def 15;

          then (( id A) . i) in ( Funcs ((A . i),(A . i))) by FUNCT_2: 9;

          hence thesis by A1, PBOOLE:def 17;

        end;

        hence thesis by PBOOLE:def 13;

      end;

    end

    definition

      let I be set;

      let D be ManySortedSet of I;

      let A be non empty Subset of ( MSFuncs (D,D));

      :: original: Element

      redefine

      mode Element of A -> ManySortedFunction of D, D ;

      coherence

      proof

        let f be Element of A;

        thus thesis by Th19;

      end;

    end

    registration

      let I, A;

      cluster ( id A) -> "onto";

      coherence

      proof

        let i be set;

        assume i in I;

        then (( id A) . i) = ( id (A . i)) by MSUALG_3:def 1;

        hence thesis by RELAT_1: 45;

      end;

      cluster ( id A) -> "1-1";

      coherence

      proof

        now

          let i be set;

          assume i in I;

          then (( id A) . i) = ( id (A . i)) by MSUALG_3:def 1;

          hence (( id A) . i) is one-to-one;

        end;

        hence thesis by MSUALG_3: 1;

      end;

    end

    begin

    reserve S for non void non empty ManySortedSign,

U1,U2 for non-empty MSAlgebra over S;

    definition

      let S, U1, U2;

      mode MSFunctionSet of U1,U2 is non empty Subset of ( MSFuncs (the Sorts of U1,the Sorts of U2));

    end

    theorem :: AUTALG_1:21

    ( id the Sorts of U1) in ( MSFuncs (the Sorts of U1,the Sorts of U1)) by Th20;

    definition

      let S, U1;

      set T = the Sorts of U1;

      :: AUTALG_1:def5

      func MSAAut U1 -> MSFunctionSet of U1, U1 means

      : Def5: for h be ManySortedFunction of U1, U1 holds h in it iff h is_isomorphism (U1,U1);

      existence

      proof

        defpred P[ object] means ex msf be ManySortedFunction of U1, U1 st $1 = msf & msf is_isomorphism (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;



         A2: X c= ( MSFuncs (T,T)) by A1;

        ( id T) in ( MSFuncs (T,T)) & ex F be ManySortedFunction of U1, U1 st ( id T) = F & F is_isomorphism (U1,U1) by Th20, MSUALG_3: 16;

        then

        reconsider X as MSFunctionSet of U1, U1 by A1, A2;

        take X;

        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_isomorphism (U1,U1) by A1;

          hence h is_isomorphism (U1,U1);

        end;

        h in ( MSFuncs (T,T)) by Th20;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be MSFunctionSet of U1, U1 such that

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

         A4: for h be ManySortedFunction of U1, U1 holds h in F2 iff h is_isomorphism (U1,U1);

        thus F1 c= F2

        proof

          let q be object;

          assume

           A5: q in F1;

          then

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

          h1 is_isomorphism (U1,U1) by A3, A5;

          hence thesis by A4;

        end;

        let q be object;

        assume

         A6: q in F2;

        then

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

        h1 is_isomorphism (U1,U1) by A4, A6;

        hence thesis by A3;

      end;

    end

    theorem :: AUTALG_1:22

    for f be Element of ( MSAAut U1) holds f in ( MSFuncs (the Sorts of U1,the Sorts of U1)) by Th20;

    theorem :: AUTALG_1:23

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



     Lm3: for f be Element of ( MSAAut U1) holds f is "1-1" & f is "onto"

    proof

      let f be Element of ( MSAAut U1);

      f is_isomorphism (U1,U1) by Def5;

      hence thesis by MSUALG_3: 13;

    end;

    theorem :: AUTALG_1:24



     Th24: ( id the Sorts of U1) in ( MSAAut U1)

    proof

      ( id the Sorts of U1) is_isomorphism (U1,U1) by MSUALG_3: 16;

      hence thesis by Def5;

    end;

    theorem :: AUTALG_1:25



     Th25: for f be Element of ( MSAAut U1) holds (f "" ) in ( MSAAut U1)

    proof

      let f be Element of ( MSAAut U1);

      f is_isomorphism (U1,U1) by Def5;

      then (f "" ) is_isomorphism (U1,U1) by MSUALG_3: 14;

      hence thesis by Def5;

    end;

    theorem :: AUTALG_1:26



     Th26: for f1,f2 be Element of ( MSAAut U1) holds (f1 ** f2) in ( MSAAut U1)

    proof

      let f1,f2 be Element of ( MSAAut U1);

      f1 is_isomorphism (U1,U1) & f2 is_isomorphism (U1,U1) by Def5;

      then (f1 ** f2) is_isomorphism (U1,U1) by MSUALG_3: 15;

      hence thesis by Def5;

    end;

    theorem :: AUTALG_1:27



     Th27: for F be ManySortedFunction of ( MSAlg UA), ( MSAlg UA) holds for f be Element of ( UAAut UA) st F = ( 0 .--> f) holds F in ( MSAAut ( MSAlg UA))

    proof

      let F be ManySortedFunction of ( MSAlg UA), ( MSAlg UA);

      let f be Element of ( UAAut UA);

      assume F = ( 0 .--> f);

      then

       A1: F = ( MSAlg f) by MSUHOM_1:def 3;

      f is_isomorphism by Def1;

      then ( MSAlg f) is_isomorphism (( MSAlg UA),(( MSAlg UA) Over ( MSSign UA))) by MSUHOM_1: 20;

      then F is_isomorphism (( MSAlg UA),( MSAlg UA)) by A1, MSUHOM_1: 9;

      hence thesis by Def5;

    end;

    definition

      let S, U1;

      :: AUTALG_1:def6

      func MSAAutComp U1 -> BinOp of ( MSAAut U1) means

      : Def6: for x,y be Element of ( MSAAut U1) holds (it . (x,y)) = (y ** x);

      existence

      proof

        defpred P[ Element of ( MSAAut U1), Element of ( MSAAut U1), set] means $3 = ($2 ** $1);



         A1: for x,y be Element of ( MSAAut U1) holds ex m be Element of ( MSAAut U1) st P[x, y, m]

        proof

          let x,y be Element of ( MSAAut U1);

          reconsider xx = x, yy = y as ManySortedFunction of U1, U1;

          reconsider m = (yy ** xx) as Element of ( MSAAut U1) by Th26;

          take m;

          thus thesis;

        end;

        thus ex IT be BinOp of ( MSAAut U1) st for x,y be Element of ( MSAAut U1) holds P[x, y, (IT . (x,y))] from BINOP_1:sch 3( A1);

      end;

      uniqueness

      proof

        let b1,b2 be BinOp of ( MSAAut U1) such that

         A2: for x,y be Element of ( MSAAut U1) holds (b1 . (x,y)) = (y ** x) and

         A3: for x,y be Element of ( MSAAut U1) holds (b2 . (x,y)) = (y ** x);

        for x,y be Element of ( MSAAut U1) holds (b1 . (x,y)) = (b2 . (x,y))

        proof

          let x,y be Element of ( MSAAut 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;

      :: AUTALG_1:def7

      func MSAAutGroup U1 -> Group equals multMagma (# ( MSAAut U1), ( MSAAutComp U1) #);

      coherence

      proof

        set SO = the Sorts of U1;

        set H = multMagma (# ( MSAAut U1), ( MSAAutComp U1) #);



         A1: ex e be Element of H st for h be Element of H holds (h * e) = h & (e * h) = h & ex g be Element of H st (h * g) = e & (g * h) = e

        proof

          reconsider e = ( id SO) as Element of H by Th24;

          take e;

          let h be Element of H;

          consider A be Element of ( MSAAut U1) such that

           A2: A = h;

          (h * e) = (( id SO) ** A) by A2, Def6

          .= A by MSUALG_3: 4;

          hence (h * e) = h by A2;

          (e * h) = (A ** ( id SO)) by A2, Def6

          .= A by MSUALG_3: 3;

          hence (e * h) = h by A2;

          reconsider g = (A "" ) as Element of H by Th25;

          take g;



           A3: A is "onto" & A is "1-1" by Lm3;



          thus (h * g) = ((A "" ) ** A) by A2, Def6

          .= e by A3, MSUALG_3: 5;



          thus (g * h) = (A ** (A "" )) by A2, Def6

          .= e by A3, MSUALG_3: 5;

        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 ( MSAAut U1);



           A4: (g * h) = (C ** B) by Def6;

          (f * g) = (B ** A) by Def6;



          hence ((f * g) * h) = (C ** (B ** A)) by Def6

          .= ((C ** B) ** A) by PBOOLE: 140

          .= (f * (g * h)) by A4, Def6;

        end;

        hence thesis by A1, GROUP_1:def 2, GROUP_1:def 3;

      end;

    end

    registration

      let S, U1;

      cluster ( MSAAutGroup U1) -> strict;

      coherence ;

    end

    theorem :: AUTALG_1:28

    for x,y be Element of ( MSAAutGroup U1) holds for f,g be Element of ( MSAAut U1) st x = f & y = g holds (x * y) = (g ** f) by Def6;

    theorem :: AUTALG_1:29



     Th29: ( id the Sorts of U1) = ( 1_ ( MSAAutGroup U1))

    proof

      set T = the Sorts of U1;

      set f = the Element of ( MSAAutGroup U1);

      reconsider g = ( id T) as Element of ( MSAAutGroup U1) by Th24;

      consider g1 be ManySortedFunction of T, T such that

       A1: g1 = g;

      f is Element of ( MSAAut U1);

      then

      consider f1 be ManySortedFunction of T, T such that

       A2: f1 = f;

      (g * f) = (f1 ** g1) by A1, A2, Def6

      .= f by A1, A2, MSUALG_3: 3;

      hence thesis by GROUP_1: 7;

    end;

    theorem :: AUTALG_1:30

    for f be Element of ( MSAAut U1) holds for g be Element of ( MSAAutGroup U1) st f = g holds (f "" ) = (g " )

    proof

      let f be Element of ( MSAAut U1);

      let g be Element of ( MSAAutGroup U1);

      consider g1 be Element of ( MSAAut U1) such that

       A1: g1 = (g " );

      assume f = g;

      then (g1 ** f) = (g * (g " )) by A1, Def6;

      then (g1 ** f) = ( 1_ ( MSAAutGroup U1)) by GROUP_1:def 5;

      then

       A2: (g1 ** f) = ( id the Sorts of U1) by Th29;

      f is "1-1" & f is "onto" by Lm3;

      hence thesis by A1, A2, Th17;

    end;

    begin

    theorem :: AUTALG_1:31



     Th31: for UA1,UA2 be Universal_Algebra st (UA1,UA2) are_similar holds for F be ManySortedFunction of ( MSAlg UA1), (( MSAlg UA2) Over ( MSSign UA1)) holds (F . 0 ) is Function of UA1, UA2

    proof

      let UA1,UA2 be Universal_Algebra;



       A1: 0 in { 0 } by TARSKI:def 1;

      assume (UA1,UA2) are_similar ;

      then ( MSSign UA1) = ( MSSign UA2) by MSUHOM_1: 10;

      then

       A2: ( MSAlg UA2) = MSAlgebra (# ( MSSorts UA2), ( MSCharact UA2) #) & (( MSAlg UA2) Over ( MSSign UA1)) = ( MSAlg UA2) by MSUALG_1:def 11, MSUHOM_1: 9;

      let F be ManySortedFunction of ( MSAlg UA1), (( MSAlg UA2) Over ( MSSign UA1));



       A3: the carrier of ( MSSign UA1) = { 0 } & ( MSAlg UA1) = MSAlgebra (# ( MSSorts UA1), ( MSCharact UA1) #) by MSUALG_1:def 8, MSUALG_1:def 11;



       A4: (( MSSorts UA2) . 0 ) = (( 0 .--> the carrier of UA2) . 0 ) by MSUALG_1:def 9

      .= the carrier of UA2 by A1, FUNCOP_1: 7;

      (( MSSorts UA1) . 0 ) = (( 0 .--> the carrier of UA1) . 0 ) by MSUALG_1:def 9

      .= the carrier of UA1 by A1, FUNCOP_1: 7;

      hence thesis by A1, A3, A4, A2, PBOOLE:def 15;

    end;

    theorem :: AUTALG_1:32



     Th32: for f be Element of ( UAAut UA) holds ( 0 .--> f) is ManySortedFunction of ( MSAlg UA), ( MSAlg UA)

    proof

      let f be Element of ( UAAut UA);

      ( MSAlg f) is ManySortedFunction of ( MSAlg UA), ( MSAlg UA) by MSUHOM_1: 9;

      hence thesis by MSUHOM_1:def 3;

    end;



     Lm4: for h be Function st (( dom h) = ( UAAut UA) & for x be object st x in ( UAAut UA) holds (h . x) = ( 0 .--> x)) holds ( rng h) = ( MSAAut ( MSAlg UA))

    proof

      let h be Function such that

       A1: ( dom h) = ( UAAut UA) and

       A2: for x be object st x in ( UAAut UA) holds (h . x) = ( 0 .--> x);

      thus ( rng h) c= ( MSAAut ( MSAlg UA))

      proof

        let x be object;

        assume x in ( rng h);

        then

        consider q be object such that

         A3: q in ( dom h) and

         A4: x = (h . q) by FUNCT_1:def 3;

        consider q9 be Element of ( UAAut UA) such that

         A5: q9 = q by A1, A3;

        x = ( 0 .--> q) & ( 0 .--> q) is ManySortedFunction of ( MSAlg UA), ( MSAlg UA) by A1, A2, A3, A4, Th32;

        then

        consider d be ManySortedFunction of ( MSAlg UA), ( MSAlg UA) such that

         A6: d = x;

        q9 is_isomorphism by Def1;

        then

         A7: ( MSAlg q9) is_isomorphism (( MSAlg UA),(( MSAlg UA) Over ( MSSign UA))) by MSUHOM_1: 20;

        ( MSAlg q9) = ( 0 .--> q) by A5, MSUHOM_1:def 3

        .= x by A1, A2, A3, A4;

        then d is_isomorphism (( MSAlg UA),( MSAlg UA)) by A6, A7, MSUHOM_1: 9;

        hence thesis by A6, Def5;

      end;

      let x be object;

      assume

       A8: x in ( MSAAut ( MSAlg UA));

      then

      reconsider f = x as ManySortedFunction of ( MSAlg UA), ( MSAlg UA) by Th19;

      the carrier of ( MSSign UA) = { 0 } by MSUALG_1:def 8;

      then

       A9: f = ( 0 .--> (f . 0 )) by Th11;



       A10: f is_isomorphism (( MSAlg UA),( MSAlg UA)) by A8, Def5;

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

        ( MSAlg q9) = f by A9, MSUHOM_1:def 3;

        then ( MSAlg q9) is_isomorphism (( MSAlg UA),(( MSAlg UA) Over ( MSSign UA))) by A10, MSUHOM_1: 9;

        then q9 is_isomorphism by MSUHOM_1: 24;

        hence q in ( dom h) by A1, Def1;

        hence thesis by A1, A2, A9;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: AUTALG_1:33



     Th33: for h be Function st (( dom h) = ( UAAut UA) & for x be object st x in ( UAAut UA) holds (h . x) = ( 0 .--> x)) holds h is Homomorphism of ( UAAutGroup UA), ( MSAAutGroup ( MSAlg UA))

    proof

      let h be Function such that

       A1: ( dom h) = ( UAAut UA) and

       A2: for x be object st x in ( UAAut UA) holds (h . x) = ( 0 .--> x);

      set H = ( MSAAutGroup ( MSAlg UA));

      set G = ( UAAutGroup UA);

      ( rng h) c= the carrier of H by A1, A2, Lm4;

      then

      reconsider h9 = h as Function of G, H by A1, FUNCT_2:def 1, RELSET_1: 4;

      now

        let a,b be Element of ( UAAutGroup UA);

        thus (h9 . (a * b)) = ((h9 . a) * (h9 . b))

        proof

          reconsider a9 = a, b9 = b as Element of ( UAAut UA);



           A3: (h9 . (b9 * a9)) = ( 0 .--> (b9 * a9)) by A2, Th6;

          reconsider A = ( 0 .--> a9), B = ( 0 .--> b9) as ManySortedFunction of ( MSAlg UA), ( MSAlg UA) by Th32;

          reconsider ha = (h9 . a), hb = (h9 . b) as Element of ( MSAAut ( MSAlg UA));

          reconsider A9 = A, B9 = B as Element of ( MSAAutGroup ( MSAlg UA)) by Th27;



           A4: ha = A9 & hb = B9 by A2;



          thus (h9 . (a * b)) = (h9 . (b9 * a9)) by Def2

          .= ( MSAlg (b9 * a9)) by A3, 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 A4, Def6;

        end;

      end;

      hence thesis by GROUP_6:def 6;

    end;

    theorem :: AUTALG_1:34



     Th34: for h be Homomorphism of ( UAAutGroup UA), ( MSAAutGroup ( MSAlg UA)) st for x be object st x in ( UAAut UA) holds (h . x) = ( 0 .--> x) holds h is bijective

    proof

      let h be Homomorphism of ( UAAutGroup UA), ( MSAAutGroup ( MSAlg UA));

      set G = ( UAAutGroup UA);

      assume

       A1: for x be object st x in ( UAAut 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

         A2: (h . a) = (h . b);



         A3: (h . b) = ( 0 .--> b) by A1

        .= [: { 0 }, {b}:];

        (h . a) = ( 0 .--> a) by A1

        .= [: { 0 }, {a}:];

        then {a} = {b} by A2, A3, ZFMISC_1: 110;

        hence thesis by ZFMISC_1: 3;

      end;

      then

       A4: h is one-to-one by GROUP_6: 1;

      ( dom h) = ( UAAut UA) by FUNCT_2:def 1;

      then ( rng h) = the carrier of ( MSAAutGroup ( MSAlg UA)) by A1, Lm4;

      then h is onto;

      hence h is bijective by A4;

    end;

    theorem :: AUTALG_1:35

    (( UAAutGroup UA),( MSAAutGroup ( MSAlg UA))) are_isomorphic

    proof

      deffunc F( object) = ( 0 .--> $1);

      consider h be Function such that

       A1: ( dom h) = ( UAAut UA) & for x be object st x in ( UAAut UA) holds (h . x) = F(x) from FUNCT_1:sch 3;

      reconsider h as Homomorphism of ( UAAutGroup UA), ( MSAAutGroup ( MSAlg UA)) by A1, Th33;

      take h;

      thus thesis by A1, Th34;

    end;