msuhom_1.miz



    begin

    reserve U1,U2,U3 for Universal_Algebra,

m,n for Nat,

a for set,

A for non empty set,

h for Function of U1, U2;

    theorem :: MSUHOM_1:1

    

     Th1: for f,g be Function, C be set st ( rng f) c= C holds ((g | C) * f) = (g * f)

    proof

      let f,g be Function, C be set such that

       A1: ( rng f) c= C;

      ((g | C) * f) = (g * (C |` f)) by MONOID_1: 1

      .= (g * f) by A1, RELAT_1: 94;

      hence thesis;

    end;

    theorem :: MSUHOM_1:2

    

     Th2: for I be set, C be Subset of I holds (C * ) c= (I * )

    proof

      let I be set, C be Subset of I;

      thus (C * ) c= (I * )

      proof

        let a be object;

        assume a in (C * );

        then

        reconsider p = a as FinSequence of C by FINSEQ_1:def 11;

        ( rng p) c= I by XBOOLE_1: 1;

        then p is FinSequence of I by FINSEQ_1:def 4;

        hence thesis by FINSEQ_1:def 11;

      end;

    end;

    theorem :: MSUHOM_1:3

    for f be Function, C be set st f is Function-yielding holds (f | C) is Function-yielding;

    theorem :: MSUHOM_1:4

    

     Th4: for I be set, C be Subset of I, M be ManySortedSet of I holds ((M | C) # ) = ((M # ) | (C * ))

    proof

      let I be set, C be Subset of I, M be ManySortedSet of I;

      ( dom (M # )) = (I * ) by PARTFUN1:def 2;

      then ( dom ((M # ) | (C * ))) = (C * ) by Th2, RELAT_1: 62;

      then

      reconsider D = ((M # ) | (C * )) as ManySortedSet of (C * ) by PARTFUN1:def 2;

      

       A1: (C * ) c= (I * ) by Th2;

      for i be Element of (C * ) holds (((M # ) | (C * )) . i) = ( product ((M | C) * i))

      proof

        let i be Element of (C * );

        

         A2: ( rng i) c= C;

        i in (C * );

        then

         A3: i in ( dom D) by PARTFUN1:def 2;

        

         A4: i in (I * ) by A1;

        for a be object holds a in (D . i) iff ex g be Function st a = g & ( dom g) = ( dom ((M | C) * i)) & for a be object st a in ( dom ((M | C) * i)) holds (g . a) in (((M | C) * i) . a)

        proof

          let a be object;

          hereby

            assume a in (D . i);

            then a in ((M # ) . i) by A3, FUNCT_1: 47;

            then a in ( product (M * i)) by A4, FINSEQ_2:def 5;

            then

            consider g be Function such that

             A5: a = g and

             A6: ( dom g) = ( dom (M * i)) and

             A7: for x be object st x in ( dom (M * i)) holds (g . x) in ((M * i) . x) by CARD_3:def 5;

            take g;

            thus a = g by A5;

            ( rng i) c= C;

            hence ( dom g) = ( dom ((M | C) * i)) by A6, Th1;

            thus for a be object st a in ( dom ((M | C) * i)) holds (g . a) in (((M | C) * i) . a)

            proof

              

               A8: ( rng i) c= C;

              let a be object;

              assume a in ( dom ((M | C) * i));

              then a in ( dom (M * i)) by A8, Th1;

              then (g . a) in ((M * i) . a) by A7;

              hence thesis by A8, Th1;

            end;

          end;

          given g be Function such that

           A9: a = g and

           A10: ( dom g) = ( dom ((M | C) * i)) and

           A11: for a be object st a in ( dom ((M | C) * i)) holds (g . a) in (((M | C) * i) . a);

          

           A12: for a be object st a in ( dom (M * i)) holds (g . a) in ((M * i) . a)

          proof

            let a be object;

            assume a in ( dom (M * i));

            then a in ( dom ((M | C) * i)) by A2, Th1;

            then (g . a) in (((M | C) * i) . a) by A11;

            hence thesis by A2, Th1;

          end;

          ( dom g) = ( dom (M * i)) by A2, A10, Th1;

          then a in ( product (M * i)) by A9, A12, CARD_3:def 5;

          then a in ((M # ) . i) by A4, FINSEQ_2:def 5;

          hence thesis by A3, FUNCT_1: 47;

        end;

        hence thesis by CARD_3:def 5;

      end;

      

      hence ((M | C) # ) = D by FINSEQ_2:def 5

      .= ((M # ) | (C * ));

    end;

    definition

      let S,S9 be non empty ManySortedSign;

      :: MSUHOM_1:def1

      pred S <= S9 means the carrier of S c= the carrier of S9 & the carrier' of S c= the carrier' of S9 & (the Arity of S9 | the carrier' of S) = the Arity of S & (the ResultSort of S9 | the carrier' of S) = the ResultSort of S;

      reflexivity ;

    end

    theorem :: MSUHOM_1:5

    for S,S9,S99 be non empty ManySortedSign st S <= S9 & S9 <= S99 holds S <= S99

    proof

      let S,S9,S99 be non empty ManySortedSign;

      assume that

       A1: S <= S9 and

       A2: S9 <= S99;

      the carrier of S c= the carrier of S9 & the carrier of S9 c= the carrier of S99 by A1, A2;

      hence the carrier of S c= the carrier of S99;

      

       A3: the carrier' of S c= the carrier' of S9 by A1;

      the carrier' of S9 c= the carrier' of S99 by A2;

      hence the carrier' of S c= the carrier' of S99 by A3;

      

      thus (the Arity of S99 | the carrier' of S) = (the Arity of S99 | (the carrier' of S9 /\ the carrier' of S)) by A3, XBOOLE_1: 28

      .= the Arity of S by A1, A2, RELAT_1: 71;

      

      thus (the ResultSort of S99 | the carrier' of S) = (the ResultSort of S99 | (the carrier' of S9 /\ the carrier' of S)) by A3, XBOOLE_1: 28

      .= the ResultSort of S by A1, A2, RELAT_1: 71;

    end;

    theorem :: MSUHOM_1:6

    for S,S9 be strict non empty ManySortedSign st S <= S9 & S9 <= S holds S = S9

    proof

      let S,S9 be strict non empty ManySortedSign;

      assume that

       A1: S <= S9 and

       A2: S9 <= S;

      

       A3: the carrier' of S9 c= the carrier' of S by A2;

      

       A4: ( dom the ResultSort of S9) = the carrier' of S9 by FUNCT_2:def 1;

      (the ResultSort of S9 | the carrier' of S) = the ResultSort of S by A1;

      then

       A5: the ResultSort of S = the ResultSort of S9 by A3, A4, RELAT_1: 68;

      

       A6: ( dom the Arity of S9) = the carrier' of S9 by FUNCT_2:def 1;

      (the Arity of S9 | the carrier' of S) = the Arity of S by A1;

      then

       A7: the Arity of S = the Arity of S9 by A3, A6, RELAT_1: 68;

      the carrier' of S c= the carrier' of S9 by A1;

      then

       A8: the carrier' of S = the carrier' of S9 by A3, XBOOLE_0:def 10;

      the carrier of S c= the carrier of S9 & the carrier of S9 c= the carrier of S by A1, A2;

      hence thesis by A8, A7, A5, XBOOLE_0:def 10;

    end;

    theorem :: MSUHOM_1:7

    for g be Function, a be Element of A holds for k be Nat st 1 <= k & k <= n holds ((a .--> g) . ((n |-> a) /. k)) = g

    proof

      let g be Function;

      let a be Element of A;

      let k be Nat;

      assume 1 <= k & k <= n;

      then

       A1: k in ( Seg n) by FINSEQ_1: 1;

      then k in ( dom (n |-> a));

      

      then ((n |-> a) /. k) = ((n |-> a) . k) by PARTFUN1:def 6

      .= a by A1, FUNCOP_1: 7;

      hence thesis by FUNCOP_1: 72;

    end;

    theorem :: MSUHOM_1:8

    

     Th8: for I be set, I0 be Subset of I, A,B be ManySortedSet of I, F be ManySortedFunction of A, B holds for A0,B0 be ManySortedSet of I0 st A0 = (A | I0) & B0 = (B | I0) holds (F | I0) is ManySortedFunction of A0, B0

    proof

      let I be set, I0 be Subset of I, A,B be ManySortedSet of I, F be ManySortedFunction of A, B;

      let A0,B0 be ManySortedSet of I0 such that

       A1: A0 = (A | I0) and

       A2: B0 = (B | I0);

      reconsider G = (F | I0) as ManySortedFunction of I0;

      

       A3: ( dom A0) = I0 & ( dom (F | I0)) = I0 by PARTFUN1:def 2;

      

       A4: ( dom B0) = I0 by PARTFUN1:def 2;

      now

        let i be object;

        assume

         A5: i in I0;

        then

         A6: (B . i) = (B0 . i) by A2, A4, FUNCT_1: 47;

        (G . i) = (F . i) & (A . i) = (A0 . i) by A1, A3, A5, FUNCT_1: 47;

        hence (G . i) is Function of (A0 . i), (B0 . i) by A5, A6, PBOOLE:def 15;

      end;

      hence thesis by PBOOLE:def 15;

    end;

    definition

      let S,S9 be strict non void non empty ManySortedSign;

      let A be non-empty strict MSAlgebra over S9;

      assume

       A1: S <= S9;

      :: MSUHOM_1:def2

      func A Over S -> non-empty strict MSAlgebra over S means

      : Def2: the Sorts of it = (the Sorts of A | the carrier of S) & the Charact of it = (the Charact of A | the carrier' of S);

      existence

      proof

        set D = (the Charact of A | the carrier' of S);

        set C = (the Sorts of A | the carrier of S);

        

         A2: ( rng the Arity of S) c= (the carrier of S * );

        

         A3: the carrier' of S c= the carrier' of S9 by A1;

        then

        reconsider D as ManySortedSet of the carrier' of S;

        

         A4: the carrier of S c= the carrier of S9 by A1;

        then

        reconsider C as ManySortedSet of the carrier of S;

        ( rng the ResultSort of S) c= the carrier of S;

        

        then

         A5: (C * the ResultSort of S) = (the Sorts of A * the ResultSort of S) by Th1

        .= ((the Sorts of A * the ResultSort of S9) | the carrier' of S) by RELAT_1: 83, A1;

        ((C # ) * the Arity of S) = (((the Sorts of A # ) | (the carrier of S * )) * the Arity of S) by A4, Th4

        .= ((the Sorts of A # ) * (the Arity of S9 | the carrier' of S)) by A1, A2, Th1

        .= (((the Sorts of A # ) * the Arity of S9) | the carrier' of S) by RELAT_1: 83;

        then

        reconsider D as ManySortedFunction of ((C # ) * the Arity of S), (C * the ResultSort of S) by A3, A5, Th8;

        reconsider B = MSAlgebra (# C, D #) as non-empty strict MSAlgebra over S by MSUALG_1:def 3;

        take B;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: MSUHOM_1:9

    

     Th9: for S be strict non void non empty ManySortedSign, A be non-empty strict MSAlgebra over S holds A = (A Over S)

    proof

      let S be strict non void non empty ManySortedSign;

      let A be non-empty strict MSAlgebra over S;

      

       A1: the Charact of (A Over S) = (the Charact of A | the carrier' of S) by Def2

      .= the Charact of A;

      the Sorts of (A Over S) = (the Sorts of A | the carrier of S) by Def2

      .= the Sorts of A;

      hence thesis by A1;

    end;

    theorem :: MSUHOM_1:10

    

     Th10: for U1, U2 st (U1,U2) are_similar holds ( MSSign U1) = ( MSSign U2)

    proof

      let U1, U2 such that

       A1: (U1,U2) are_similar ;

      reconsider f = (( *--> 0 ) * ( signature U1)) as Function of ( dom ( signature U1)), ( { 0 } * ) by MSUALG_1: 2;

      

       A2: the carrier of ( MSSign U1) = { 0 } & the Arity of ( MSSign U1) = f by MSUALG_1:def 8;

      reconsider f = (( *--> 0 ) * ( signature U2)) as Function of ( dom ( signature U2)), ( { 0 } * ) by MSUALG_1: 2;

      

       A3: the Arity of ( MSSign U2) = f & the ResultSort of ( MSSign U2) = (( dom ( signature U2)) --> 0 ) by MSUALG_1:def 8;

      

       A4: the ResultSort of ( MSSign U1) = (( dom ( signature U1)) --> 0 ) & the carrier of ( MSSign U2) = { 0 } by MSUALG_1:def 8;

      the carrier' of ( MSSign U1) = ( dom ( signature U1)) & the carrier' of ( MSSign U2) = ( dom ( signature U2)) by MSUALG_1:def 8;

      then the carrier' of ( MSSign U1) = the carrier' of ( MSSign U2) by A1;

      hence thesis by A1, A2, A4, A3;

    end;

    definition

      let U1,U2 be Universal_Algebra, h be Function of U1, U2;

      assume

       A1: ( MSSign U1) = ( MSSign U2);

      :: MSUHOM_1:def3

      func MSAlg h -> ManySortedFunction of ( MSAlg U1), (( MSAlg U2) Over ( MSSign U1)) equals

      : Def3: ( 0 .--> h);

      coherence

      proof

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

        then

        reconsider Z2 = the Sorts of ( MSAlg U2) as ManySortedSet of { 0 };

        set f = ( 0 .--> h);

        ( MSAlg U2) = MSAlgebra (# ( MSSorts U2), ( MSCharact U2) #) by MSUALG_1:def 11;

        

        then

         A2: (the Sorts of ( MSAlg U2) . 0 ) = (( 0 .--> the carrier of U2) . 0 ) by MSUALG_1:def 9

        .= the carrier of U2 by FUNCOP_1: 72;

        

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

        then

        reconsider Z1 = the Sorts of ( MSAlg U1) as ManySortedSet of { 0 };

        ( MSAlg U1) = MSAlgebra (# ( MSSorts U1), ( MSCharact U1) #) by MSUALG_1:def 11;

        

        then

         A4: (the Sorts of ( MSAlg U1) . 0 ) = (( 0 .--> the carrier of U1) . 0 ) by MSUALG_1:def 9

        .= the carrier of U1 by FUNCOP_1: 72;

        now

          let a be object;

          assume a in { 0 };

          then a = 0 by TARSKI:def 1;

          hence (f . a) is Function of (the Sorts of ( MSAlg U1) . a), (the Sorts of ( MSAlg U2) . a) by A4, A2, FUNCOP_1: 72;

        end;

        then f is ManySortedFunction of Z1, Z2 by PBOOLE:def 15;

        hence thesis by A1, A3, Th9;

      end;

    end

    theorem :: MSUHOM_1:11

    

     Th11: for U1, U2, h st (U1,U2) are_similar holds for o be OperSymbol of ( MSSign U1) holds (( MSAlg h) . ( the_result_sort_of o)) = h

    proof

      let U1, U2, h such that

       A1: (U1,U2) are_similar ;

      set f = ( MSAlg h);

      let o be OperSymbol of ( MSSign U1);

      

       A2: the carrier' of ( MSSign U1) = ( dom ( signature U1)) & the ResultSort of ( MSSign U1) = (( dom ( signature U1)) --> 0 ) by MSUALG_1:def 8;

      

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

      

      thus (f . ( the_result_sort_of o)) = (f . (the ResultSort of ( MSSign U1) . o)) by MSUALG_1:def 2

      .= (( 0 .--> h) . 0 ) by A1, A2, Def3, Th10

      .= h by A3, FUNCOP_1: 7;

    end;

    theorem :: MSUHOM_1:12

    

     Th12: for o be OperSymbol of ( MSSign U1) holds ( Den (o,( MSAlg U1))) = (the charact of U1 . o)

    proof

      let o be OperSymbol of ( MSSign U1);

      ( MSAlg U1) = MSAlgebra (# ( MSSorts U1), ( MSCharact U1) #) by MSUALG_1:def 11;

      

      hence ( Den (o,( MSAlg U1))) = (( MSCharact U1) . o) by MSUALG_1:def 6

      .= (the charact of U1 . o) by MSUALG_1:def 10;

    end;

    

     Lm1: for U1 be Universal_Algebra holds ( dom ( signature U1)) = ( dom the charact of U1)

    proof

      let U1 be Universal_Algebra;

      

      thus ( dom ( signature U1)) = ( Seg ( len ( signature U1))) by FINSEQ_1:def 3

      .= ( Seg ( len the charact of U1)) by UNIALG_1:def 4

      .= ( dom the charact of U1) by FINSEQ_1:def 3;

    end;

    theorem :: MSUHOM_1:13

    

     Th13: for o be OperSymbol of ( MSSign U1) holds ( Den (o,( MSAlg U1))) is operation of U1

    proof

      let o be OperSymbol of ( MSSign U1);

      

       A1: ( dom ( signature U1)) = ( dom the charact of U1) by Lm1;

      ( Den (o,( MSAlg U1))) = (the charact of U1 . o) & the carrier' of ( MSSign U1) = ( dom ( signature U1)) by Th12, MSUALG_1:def 8;

      hence thesis by A1, FUNCT_1:def 3;

    end;

    

     Lm2: for U1, U2 st (U1,U2) are_similar holds for o be OperSymbol of ( MSSign U1) holds ( Den (o,(( MSAlg U2) Over ( MSSign U1)))) is operation of U2

    proof

      let U1, U2;

      set A = (( MSAlg U2) Over ( MSSign U1));

      

       A1: ( MSAlg U2) = MSAlgebra (# ( MSSorts U2), ( MSCharact U2) #) by MSUALG_1:def 11;

      assume

       A2: (U1,U2) are_similar ;

      then

       A3: ( MSSign U1) = ( MSSign U2) by Th10;

      let o be OperSymbol of ( MSSign U1);

      

       A4: ( Den (o,A)) = (the Charact of A . o) by MSUALG_1:def 6

      .= (( MSCharact U2) . o) by A3, A1, Th9

      .= (the charact of U2 . o) by MSUALG_1:def 10;

      

       A5: ( dom ( signature U1)) = ( dom the charact of U1) by Lm1;

      ( signature U1) = ( signature U2) by A2;

      then the carrier' of ( MSSign U1) = ( dom ( signature U1)) & ( dom the charact of U1) = ( dom the charact of U2) by A5, Lm1, MSUALG_1:def 8;

      hence thesis by A4, A5, FUNCT_1:def 3;

    end;

    theorem :: MSUHOM_1:14

    

     Th14: for o be OperSymbol of ( MSSign U1) holds for y be Element of ( Args (o,( MSAlg U1))) holds y is FinSequence of the carrier of U1

    proof

      let o be OperSymbol of ( MSSign U1);

      let y be Element of ( Args (o,( MSAlg U1)));

      set O1 = ( Den (o,( MSAlg U1)));

      

       A1: O1 = (the charact of U1 . o) & the carrier' of ( MSSign U1) = ( dom ( signature U1)) by Th12, MSUALG_1:def 8;

      ( dom ( signature U1)) = ( dom the charact of U1) by Lm1;

      then

      reconsider O1 as operation of U1 by A1, FUNCT_1:def 3;

      ( Args (o,( MSAlg U1))) = ( dom O1) by FUNCT_2:def 1;

      then y in (the carrier of U1 * ) by TARSKI:def 3;

      hence thesis by FINSEQ_1:def 11;

    end;

    theorem :: MSUHOM_1:15

    

     Th15: for U1, U2, h st (U1,U2) are_similar holds for o be OperSymbol of ( MSSign U1), y be Element of ( Args (o,( MSAlg U1))) holds (( MSAlg h) # y) = (h * y)

    proof

      let U1, U2, h;

      assume

       A1: (U1,U2) are_similar ;

      reconsider f1 = (( *--> 0 ) * ( signature U1)) as Function of ( dom ( signature U1)), ( { 0 } * ) by MSUALG_1: 2;

      let o be OperSymbol of ( MSSign U1);

      

       A2: the carrier' of ( MSSign U2) = ( dom ( signature U2)) by MSUALG_1:def 8;

      ( MSSign U1) = ( MSSign U2) by A1, Th10;

      then o in ( dom ( signature U2)) by A2;

      then

       A3: o in ( dom ( signature U1)) by A1;

      then o in ( dom f1) by FUNCT_2:def 1;

      then

       A4: ((( *--> 0 ) * ( signature U1)) . o) = (( *--> 0 ) . (( signature U1) . o)) by FUNCT_1: 12;

      let y be Element of ( Args (o,( MSAlg U1)));

      set f = ( MSAlg h);

      

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

      set X = ( dom (h * y));

      

       A6: ( dom h) = the carrier of U1 by FUNCT_2:def 1;

      

       A7: y is FinSequence of the carrier of U1 by Th14;

      then ( rng y) c= the carrier of U1 by FINSEQ_1:def 4;

      then

      reconsider p = (h * y) as FinSequence by A7, A6, FINSEQ_1: 16;

      

       A8: X = ( dom y) by A7, FINSEQ_3: 120;

      the Arity of ( MSSign U1) = f1 by MSUALG_1:def 8;

      then

       A9: ( the_arity_of o) = ((( *--> 0 ) * ( signature U1)) . o) by MSUALG_1:def 1;

      (( signature U1) . o) in ( rng ( signature U1)) by A3, FUNCT_1:def 3;

      then

      consider n be Element of NAT such that

       A10: n = (( signature U1) . o);

      

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

       A12:

      now

         0 is Element of { 0 } by TARSKI:def 1;

        then (n |-> 0 ) is FinSequence of { 0 } by FINSEQ_2: 63;

        then

        reconsider l = (n |-> 0 ) as Element of (the carrier of ( MSSign U1) * ) by A5, FINSEQ_1:def 11;

        let m;

        

         A13: (( the_arity_of o) /. m) = (l /. m) & ( dom (n |-> 0 )) = ( Seg n) by A9, A4, A10, FINSEQ_2:def 6;

        assume m in ( dom y);

        then m in ( dom ( the_arity_of o)) by MSUALG_3: 6;

        then

         A14: m in ( dom (n |-> 0 )) by A9, A4, A10, FINSEQ_2:def 6;

        then (l /. m) = (l . m) by PARTFUN1:def 6;

        then (( the_arity_of o) /. m) = 0 by A14, A13, FUNCOP_1: 7;

        

        hence (f . (( the_arity_of o) /. m)) = (( 0 .--> h) . 0 ) by A1, Def3, Th10

        .= h by A11, FUNCOP_1: 7;

      end;

       A15:

      now

        let m be Nat;

        assume

         A16: m in ( dom y);

        then

         A17: m in ( dom (h * y)) by A7, FINSEQ_3: 120;

        ((f # y) . m) = ((f . (( the_arity_of o) /. m)) . (y . m)) by A16, MSUALG_3:def 6;

        

        hence ((f # y) . m) = (h . (y . m)) by A12, A16

        .= (p . m) by A7, A17, FINSEQ_3: 120;

      end;

      ( dom (f # y)) = ( dom ( the_arity_of o)) by MSUALG_3: 6

      .= ( dom (n |-> 0 )) by A9, A4, A10, FINSEQ_2:def 6

      .= ( Seg n);

      then

       A18: (f # y) is FinSequence by FINSEQ_1:def 2;

      

       A19: ( dom y) = ( dom ( the_arity_of o)) by MSUALG_3: 6

      .= ( dom (n |-> 0 )) by A9, A4, A10, FINSEQ_2:def 6

      .= ( Seg n);

      ( dom (f # y)) = ( dom ( the_arity_of o)) by MSUALG_3: 6

      .= ( dom (n |-> 0 )) by A9, A4, A10, FINSEQ_2:def 6

      .= X by A7, A19, FINSEQ_3: 120;

      hence thesis by A18, A15, A8, FINSEQ_1: 13;

    end;

    theorem :: MSUHOM_1:16

    

     Th16: h is_homomorphism implies ( MSAlg h) is_homomorphism (( MSAlg U1),(( MSAlg U2) Over ( MSSign U1)))

    proof

      set f = ( MSAlg h);

      set A = (( MSAlg U2) Over ( MSSign U1));

      

       A1: ( MSAlg U2) = MSAlgebra (# ( MSSorts U2), ( MSCharact U2) #) by MSUALG_1:def 11;

      consider m such that

       A2: the carrier' of ( MSSign U1) = ( Seg m) by MSUALG_1:def 7;

      assume

       A3: h is_homomorphism ;

      then

       A4: (U1,U2) are_similar ;

      then

       A5: ( MSSign U1) = ( MSSign U2) by Th10;

      let o be OperSymbol of ( MSSign U1) such that ( Args (o,( MSAlg U1))) <> {} ;

      o in ( Seg m) by A2;

      then

      reconsider k = o as Element of NAT ;

      reconsider O2 = ( Den (o,A)) as operation of U2 by A4, Lm2;

      ( Den (o,A)) = (the Charact of A . o) by MSUALG_1:def 6

      .= (( MSCharact U2) . o) by A5, A1, Th9

      .= (the charact of U2 . o) by MSUALG_1:def 10;

      then

       A6: O2 = (the charact of U2 . k);

      set O1 = ( Den (o,( MSAlg U1)));

      let y be Element of ( Args (o,( MSAlg U1)));

      

       A7: O1 = (the charact of U1 . o) & the carrier' of ( MSSign U1) = ( dom ( signature U1)) by Th12, MSUALG_1:def 8;

      reconsider O1 as operation of U1 by Th13;

      

       A8: y is FinSequence of the carrier of U1 by Th14;

      ( dom ( signature U1)) = ( dom the charact of U1) & ( Args (o,( MSAlg U1))) = ( dom O1) by Lm1, FUNCT_2:def 1;

      

      then (h . (O1 . y)) = (O2 . (h * y)) by A3, A7, A6, A8

      .= (( Den (o,A)) . (f # y)) by A4, Th15;

      hence thesis by A4, Th11;

    end;

    

     Lm3: for n be Nat st n in ( dom the charact of U1) holds n is OperSymbol of ( MSSign U1)

    proof

      

       A1: ( dom ( signature U1)) = ( dom the charact of U1) by Lm1;

      let n be Nat;

      assume n in ( dom the charact of U1);

      hence thesis by A1, MSUALG_1:def 8;

    end;

    theorem :: MSUHOM_1:17

    

     Th17: (U1,U2) are_similar implies ( MSAlg h) is ManySortedSet of { 0 }

    proof

      assume (U1,U2) are_similar ;

      then ( MSAlg h) = ( 0 .--> h) by Def3, Th10;

      hence thesis;

    end;

    theorem :: MSUHOM_1:18

    

     Th18: h is_epimorphism implies ( MSAlg h) is_epimorphism (( MSAlg U1),(( MSAlg U2) Over ( MSSign U1)))

    proof

      set f = ( MSAlg h);

      set A = (( MSAlg U2) Over ( MSSign U1));

      

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

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

      then

       A2: the carrier of ( MSSign U1) = { 0 } & (( MSSorts U2) . 0 ) = the carrier of U2 by A1, FUNCOP_1: 7, MSUALG_1:def 8;

      

       A3: ( MSAlg U2) = MSAlgebra (# ( MSSorts U2), ( MSCharact U2) #) by MSUALG_1:def 11;

      assume

       A4: h is_epimorphism ;

      then

       A5: ( rng h) = the carrier of U2;

      

       A6: h is_homomorphism by A4;

      then

       A7: (U1,U2) are_similar ;

      then ( MSSign U1) = ( MSSign U2) by Th10;

      then

       A8: the Sorts of A = ( MSSorts U2) by A3, Th9;

      thus f is_homomorphism (( MSAlg U1),A) by A6, Th16;

      let i be set;

      assume i in the carrier of ( MSSign U1);

      then

      reconsider i9 = i as Element of ( MSSign U1);

      reconsider h9 = (f . i) as Function of (the Sorts of ( MSAlg U1) . i9), (the Sorts of A . i9) by PBOOLE:def 15;

      (f . 0 ) = (( 0 .--> h) . 0 ) by A7, Def3, Th10

      .= h by A1, FUNCOP_1: 7;

      then the carrier of ( MSSign U1) = { 0 } & ( rng h9) = (the Sorts of A . 0 ) by A5, A8, A2, TARSKI:def 1;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: MSUHOM_1:19

    

     Th19: h is_monomorphism implies ( MSAlg h) is_monomorphism (( MSAlg U1),(( MSAlg U2) Over ( MSSign U1)))

    proof

      set f = ( MSAlg h);

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

      then

       A1: ( dom f) = { 0 } by PARTFUN1:def 2;

      assume

       A2: h is_monomorphism ;

      then

       A3: h is_homomorphism ;

      hence ( MSAlg h) is_homomorphism (( MSAlg U1),(( MSAlg U2) Over ( MSSign U1))) by Th16;

      (U1,U2) are_similar by A3;

      then f = ( 0 .--> h) by Def3, Th10;

      then

       A4: (f . 0 ) = h by FUNCOP_1: 72;

      let i be set, h9 be Function;

      assume i in ( dom f) & (f . i) = h9;

      then h = h9 by A4, A1, TARSKI:def 1;

      hence thesis by A2;

    end;

    theorem :: MSUHOM_1:20

    h is_isomorphism implies ( MSAlg h) is_isomorphism (( MSAlg U1),(( MSAlg U2) Over ( MSSign U1))) by Th18, Th19;

    theorem :: MSUHOM_1:21

    

     Th21: for U1, U2, h st (U1,U2) are_similar holds ( MSAlg h) is_homomorphism (( MSAlg U1),(( MSAlg U2) Over ( MSSign U1))) implies h is_homomorphism

    proof

      let U1, U2, h such that

       A1: (U1,U2) are_similar ;

      

       A2: ( MSSign U1) = ( MSSign U2) by A1, Th10;

      set A = (( MSAlg U2) Over ( MSSign U1));

      set f = ( MSAlg h);

      assume

       A3: f is_homomorphism (( MSAlg U1),A);

      thus (U1,U2) are_similar by A1;

      let n be Nat;

      assume n in ( dom the charact of U1);

      then

      reconsider o = n as OperSymbol of ( MSSign U1) by Lm3;

      let O1 be operation of U1, O2 be operation of U2 such that

       A4: O1 = (the charact of U1 . n) and

       A5: O2 = (the charact of U2 . n);

      

       A6: O1 = ( Den (o,( MSAlg U1))) by A4, Th12;

      let x be FinSequence of U1;

      assume x in ( dom O1);

      then

      reconsider y = x as Element of ( Args (o,( MSAlg U1))) by A6, FUNCT_2:def 1;

      

       A7: ((f . ( the_result_sort_of o)) . (( Den (o,( MSAlg U1))) . y)) = (h . (O1 . y)) by A1, A6, Th11;

      

       A8: ((f . ( the_result_sort_of o)) . (( Den (o,( MSAlg U1))) . y)) = (( Den (o,A)) . (f # y)) by A3;

      

       A9: ( MSAlg U2) = MSAlgebra (# ( MSSorts U2), ( MSCharact U2) #) by MSUALG_1:def 11;

      ( Den (o,A)) = (the Charact of A . o) by MSUALG_1:def 6

      .= (( MSCharact U2) . o) by A2, A9, Th9

      .= O2 by A5, MSUALG_1:def 10;

      hence thesis by A1, A7, A8, Th15;

    end;

    theorem :: MSUHOM_1:22

    

     Th22: for U1, U2, h st (U1,U2) are_similar holds ( MSAlg h) is_epimorphism (( MSAlg U1),(( MSAlg U2) Over ( MSSign U1))) implies h is_epimorphism

    proof

      let U1, U2, h;

      set B = the Sorts of (( MSAlg U2) Over ( MSSign U1));

      set I = the carrier of ( MSSign U1);

      

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

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

      then

       A2: (( MSSorts U2) . 0 ) = the carrier of U2 by A1, FUNCOP_1: 7;

      

       A3: I = { 0 } & ( MSAlg U2) = MSAlgebra (# ( MSSorts U2), ( MSCharact U2) #) by MSUALG_1:def 8, MSUALG_1:def 11;

      assume

       A4: (U1,U2) are_similar ;

      then ( MSSign U1) = ( MSSign U2) by Th10;

      then

       A5: B = the Sorts of ( MSAlg U2) by Th9;

      assume

       A6: ( MSAlg h) is_epimorphism (( MSAlg U1),(( MSAlg U2) Over ( MSSign U1)));

      then

       A7: ( MSAlg h) is "onto";

      ( MSAlg h) is_homomorphism (( MSAlg U1),(( MSAlg U2) Over ( MSSign U1))) by A6;

      then

       A8: h is_homomorphism by A4, Th21;

      (( MSAlg h) . 0 ) = (( 0 .--> h) . 0 ) by A4, Def3, Th10

      .= h by A1, FUNCOP_1: 7;

      then ( rng h) = the carrier of U2 by A7, A1, A2, A5, A3;

      hence h is_epimorphism by A8;

    end;

    theorem :: MSUHOM_1:23

    

     Th23: for U1, U2, h st (U1,U2) are_similar holds ( MSAlg h) is_monomorphism (( MSAlg U1),(( MSAlg U2) Over ( MSSign U1))) implies h is_monomorphism

    proof

      let U1, U2, h;

      assume

       A1: (U1,U2) are_similar ;

      assume

       A2: ( MSAlg h) is_monomorphism (( MSAlg U1),(( MSAlg U2) Over ( MSSign U1)));

      then

       A3: ( MSAlg h) is "1-1";

      ( MSAlg h) is_homomorphism (( MSAlg U1),(( MSAlg U2) Over ( MSSign U1))) by A2;

      then

       A4: h is_homomorphism by A1, Th21;

      

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

      

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

      (( MSAlg h) . 0 ) = (( 0 .--> h) . 0 ) by A1, Def3, Th10

      .= h by A6, FUNCOP_1: 7;

      then h is one-to-one by A3, A5, A6, MSUALG_3: 1;

      hence thesis by A4;

    end;

    theorem :: MSUHOM_1:24

    for U1, U2, h st (U1,U2) are_similar holds ( MSAlg h) is_isomorphism (( MSAlg U1),(( MSAlg U2) Over ( MSSign U1))) implies h is_isomorphism by Th23, Th22;

    theorem :: MSUHOM_1:25

    ( MSAlg ( id the carrier of U1)) = ( id the Sorts of ( MSAlg U1))

    proof

      set f = ( id the Sorts of ( MSAlg U1));

      set h = ( id the carrier of U1);

      

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

      then

      reconsider Z1 = the Sorts of ( MSAlg U1) as ManySortedSet of { 0 };

       A2:

      now

        let i be set;

        ( MSAlg U1) = MSAlgebra (# ( MSSorts U1), ( MSCharact U1) #) by MSUALG_1:def 11;

        

        then

         A3: (Z1 . 0 ) = (( 0 .--> the carrier of U1) . 0 ) by MSUALG_1:def 9

        .= the carrier of U1 by FUNCOP_1: 72;

        assume

         A4: i in { 0 };

        then i = 0 by TARSKI:def 1;

        hence (f . 0 ) = h by A1, A4, A3, MSUALG_3:def 1;

      end;

      ( MSAlg h) = ( 0 .--> h) by Def3;

      then

       A5: (( MSAlg h) . 0 ) = h by FUNCOP_1: 72;

      now

        let a be object;

        assume

         A6: a in { 0 };

        then a = 0 by TARSKI:def 1;

        hence (f . a) = (( MSAlg h) . a) by A2, A5, A6;

      end;

      hence f = ( MSAlg h) by A1, PBOOLE: 3;

    end;

    theorem :: MSUHOM_1:26

    for U1, U2, U3 st (U1,U2) are_similar & (U2,U3) are_similar holds for h1 be Function of U1, U2, h2 be Function of U2, U3 holds (( MSAlg h2) ** ( MSAlg h1)) = ( MSAlg (h2 * h1))

    proof

      let U1, U2, U3 such that

       A1: (U1,U2) are_similar and

       A2: (U2,U3) are_similar ;

      let h1 be Function of U1, U2, h2 be Function of U2, U3;

      

       A3: ( MSAlg h1) is ManySortedSet of { 0 } by A1, Th17;

      ( MSAlg h2) is ManySortedSet of { 0 } by A2, Th17;

      then

       A4: ( dom ( MSAlg h2)) = { 0 } by PARTFUN1:def 2;

      

       A5: ( dom (( MSAlg h2) ** ( MSAlg h1))) = (( dom ( MSAlg h1)) /\ ( dom ( MSAlg h2))) by PBOOLE:def 19

      .= ( { 0 } /\ { 0 }) by A3, A4, PARTFUN1:def 2

      .= { 0 };

       A6:

      now

        let a be set, f be Function, g be Function such that

         A7: a in ( dom (( MSAlg h2) ** ( MSAlg h1))) and

         A8: f = (( MSAlg h1) . a) and

         A9: g = (( MSAlg h2) . a);

        

         A10: g = (( MSAlg h2) . 0 ) by A5, A7, A9, TARSKI:def 1

        .= (( 0 .--> h2) . 0 ) by A2, Def3, Th10

        .= h2 by FUNCOP_1: 72;

        f = (( MSAlg h1) . 0 ) by A5, A7, A8, TARSKI:def 1

        .= (( 0 .--> h1) . 0 ) by A1, Def3, Th10

        .= h1 by FUNCOP_1: 72;

        hence ((( MSAlg h2) ** ( MSAlg h1)) . a) = (h2 * h1) by A7, A8, A9, A10, PBOOLE:def 19;

      end;

      set h = (h2 * h1);

      

       A11: ( MSAlg h) is ManySortedSet of { 0 } by A1, A2, Th17, UNIALG_2: 2;

      

       A12: ( MSSign U2) = ( MSSign U3) by A2, Th10;

       A13:

      now

        let a be set;

        assume a in ( dom ( MSAlg h));

        then

         A14: a in { 0 } by A11, PARTFUN1:def 2;

        (( MSAlg (h2 * h1)) . 0 ) = (( 0 .--> (h2 * h1)) . 0 ) by A1, A12, Def3, Th10

        .= (h2 * h1) by FUNCOP_1: 72;

        hence (( MSAlg (h2 * h1)) . a) = (h2 * h1) by A14, TARSKI:def 1;

      end;

      

       A15: ( dom ( MSAlg (h2 * h1))) = { 0 } by A11, PARTFUN1:def 2;

       A16:

      now

        let a be set, f,g be Function such that

         A17: a in ( dom ( MSAlg (h2 * h1))) and

         A18: f = (( MSAlg h1) . a) & g = (( MSAlg h2) . a);

        

        thus (( MSAlg (h2 * h1)) . a) = (h2 * h1) by A13, A17

        .= ((( MSAlg h2) ** ( MSAlg h1)) . a) by A5, A6, A15, A17, A18;

      end;

      

       A19: ( dom ( MSAlg (h2 * h1))) = { 0 } by A11, PARTFUN1:def 2;

      

       A20: for a be object st a in { 0 } holds ((( MSAlg h2) ** ( MSAlg h1)) . a) = (( MSAlg (h2 * h1)) . a)

      proof

        let a be object;

        

         A21: (( MSAlg h1) . a) is Function & (( MSAlg h2) . a) is Function;

        assume a in { 0 };

        hence thesis by A19, A16, A21;

      end;

      (( MSAlg h2) ** ( MSAlg h1)) is ManySortedSet of { 0 } by A5, PARTFUN1:def 2, RELAT_1:def 18;

      hence thesis by A11, A20, PBOOLE: 3;

    end;