msualg_3.miz



    begin

    reserve S for non void non empty ManySortedSign,

U1,U2 for MSAlgebra over S,

o for OperSymbol of S,

n for Nat;

    definition

      let I be non empty set, A,B be ManySortedSet of I, F be ManySortedFunction of A, B, i be Element of I;

      :: original: .

      redefine

      func F . i -> Function of (A . i), (B . i) ;

      coherence by PBOOLE:def 15;

    end

    definition

      let S be non empty ManySortedSign;

      let U1,U2 be MSAlgebra over S;

      mode ManySortedFunction of U1,U2 is ManySortedFunction of the Sorts of U1, the Sorts of U2;

    end

    definition

      let I be set, A be ManySortedSet of I;

      :: MSUALG_3:def1

      func id A -> ManySortedFunction of A, A means

      : Def1: for i be set st i in I holds (it . i) = ( id (A . i));

      existence

      proof

        deffunc F( object) = ( id (A . $1));

        consider f be Function such that

         A1: ( dom f) = I & for i be object st i in I holds (f . i) = F(i) from FUNCT_1:sch 3;

        reconsider f as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;

        for x be object st x in ( dom f) holds (f . x) is Function

        proof

          let x be object;

          assume x in ( dom f);

          then (f . x) = ( id (A . x)) by A1;

          hence thesis;

        end;

        then

        reconsider f as ManySortedFunction of I by FUNCOP_1:def 6;

        for i be object st i in I holds (f . i) is Function of (A . i), (A . i)

        proof

          let i be object;

          assume i in I;

          then (f . i) = ( id (A . i)) by A1;

          hence thesis;

        end;

        then

        reconsider f as ManySortedFunction of A, A by PBOOLE:def 15;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F,G be ManySortedFunction of A, A;

        assume that

         A2: for i be set st i in I holds (F . i) = ( id (A . i)) and

         A3: for i be set st i in I holds (G . i) = ( id (A . i));

         A4:

        now

          let i be object;

          assume

           A5: i in I;

          then (F . i) = ( id (A . i)) by A2;

          hence (F . i) = (G . i) by A3, A5;

        end;

        ( dom F) = I & ( dom G) = I by PARTFUN1:def 2;

        hence thesis by A4, FUNCT_1: 2;

      end;

    end

    definition

      let IT be Function;

      :: MSUALG_3:def2

      attr IT is "1-1" means for i be set, f be Function st i in ( dom IT) & (IT . i) = f holds f is one-to-one;

    end

    registration

      let I be set;

      cluster "1-1" for ManySortedFunction of I;

      existence

      proof

        set A = the ManySortedSet of I;

        take F = ( id A);

        let i be set, f be Function;

        

         A1: ( dom ( id A)) = I by PARTFUN1:def 2;

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

        then f = ( id (A . i)) by A1, Def1;

        hence thesis;

      end;

    end

    theorem :: MSUALG_3:1

    

     Th1: for I be set, F be ManySortedFunction of I holds F is "1-1" iff for i be set st i in I holds (F . i) is one-to-one

    proof

      let I be set;

      let F be ManySortedFunction of I;

      

       A1: ( dom F) = I by PARTFUN1:def 2;

      hence F is "1-1" implies for i be set st i in I holds (F . i) is one-to-one;

      assume for i be set st i in I holds (F . i) is one-to-one;

      then for i be set, f be Function st i in ( dom F) & f = (F . i) holds f is one-to-one by A1;

      hence thesis;

    end;

    definition

      let I be set, A,B be ManySortedSet of I;

      let IT be ManySortedFunction of A, B;

      :: MSUALG_3:def3

      attr IT is "onto" means for i be set st i in I holds ( rng (IT . i)) = (B . i);

    end

    theorem :: MSUALG_3:2

    

     Th2: for I be set, A,B,C be ManySortedSet of I, F be ManySortedFunction of A, B, G be ManySortedFunction of B, C holds ( dom (G ** F)) = I & for i be set st i in I holds ((G ** F) . i) = ((G . i) * (F . i))

    proof

      let I be set, A,B,C be ManySortedSet of I, F be ManySortedFunction of A, B, G be ManySortedFunction of B, C;

      ( dom F) = I & ( dom G) = I by PARTFUN1:def 2;

      then (( dom F) /\ ( dom G)) = I;

      hence

       A1: ( dom (G ** F)) = I by PBOOLE:def 19;

      let i be set;

      thus thesis by A1, PBOOLE:def 19;

    end;

    definition

      let I be set, A be ManySortedSet of I, B,C be non-empty ManySortedSet of I, F be ManySortedFunction of A, B, G be ManySortedFunction of B, C;

      :: original: **

      redefine

      func G ** F -> ManySortedFunction of A, C ;

      coherence

      proof

        ( dom (G ** F)) = I by Th2;

        then

        reconsider fg = (G ** F) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

        reconsider fg as ManySortedFunction of I;

        for i be object st i in I holds (fg . i) is Function of (A . i), (C . i)

        proof

          let i be object;

          assume

           A1: 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 A1, PBOOLE:def 15;

          ((G ** F) . i) = (g * f) by A1, Th2;

          hence thesis by A1;

        end;

        hence thesis by PBOOLE:def 15;

      end;

    end

    theorem :: MSUALG_3:3

    for I be set, A,B be ManySortedSet of I, F be ManySortedFunction of A, B holds (F ** ( id A)) = F

    proof

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

      ( dom (F ** ( id A))) = (( dom F) /\ ( dom ( id A))) by PBOOLE:def 19

      .= (I /\ ( dom ( id A))) by PARTFUN1:def 2

      .= (I /\ I) by PARTFUN1:def 2

      .= I;

      then

      reconsider G = (F ** ( id A)) as ManySortedFunction of I by PARTFUN1:def 2, RELAT_1:def 18;

      now

        let i be object;

        assume

         A1: i in I;

        then

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

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

        

         A2: (G . i) = (f * g) by A1, Th2

        .= (f * ( id (A . i))) by A1, Def1;

        per cases ;

          suppose (B . i) = {} implies (A . i) = {} ;

          then ( dom f) = (A . i) by FUNCT_2:def 1;

          hence (G . i) = (F . i) by A2, RELAT_1: 52;

        end;

          suppose (B . i) = {} & (A . i) <> {} ;

          then f = {} ;

          hence (G . i) = (F . i) by A2;

        end;

      end;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: MSUALG_3:4

    

     Th4: for I be set, A,B be ManySortedSet of I holds for F be ManySortedFunction of A, B holds (( id B) ** F) = F

    proof

      let I be set;

      let A,B be ManySortedSet of I;

      let F be ManySortedFunction of A, B;

      ( dom (( id B) ** F)) = (( dom ( id B)) /\ ( dom F)) by PBOOLE:def 19

      .= (I /\ ( dom F)) by PARTFUN1:def 2

      .= (I /\ I) by PARTFUN1:def 2

      .= I;

      then

      reconsider G = (( id B) ** F) as ManySortedFunction of I by PARTFUN1:def 2, RELAT_1:def 18;

      now

        let i be object;

        assume

         A1: i in I;

        then

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

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

        g = ( id (B . i)) & (G . i) = (g * f) by A1, Def1, Th2;

        hence (G . i) = (F . i) by FUNCT_2: 17;

      end;

      hence thesis by PBOOLE: 3;

    end;

    definition

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

      assume that

       A1: F is "1-1" and

       A2: F is "onto";

      :: MSUALG_3:def4

      func F "" -> ManySortedFunction of B, A means

      : Def4: for i be set st i in I holds (it . i) = ((F . i) " );

      existence

      proof

        defpred P[ object, object] means $2 = ((F . $1) " );

        

         A3: for i be object st i in I holds ex u be object st P[i, u];

        consider H be Function such that

         A4: ( dom H) = I & for i be object st i in I holds P[i, (H . i)] from CLASSES1:sch 1( A3);

        reconsider H as ManySortedSet of I by A4, PARTFUN1:def 2, RELAT_1:def 18;

        for x be object st x in ( dom H) holds (H . x) is Function

        proof

          let x be object;

          assume

           A5: x in ( dom H);

          then x in I by PARTFUN1:def 2;

          then

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

          (H . x) = (f " ) by A4, A5;

          hence thesis;

        end;

        then

        reconsider H as ManySortedFunction of I by FUNCOP_1:def 6;

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

        proof

          let i be object;

          assume

           A6: i in I;

          then

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

          i in ( dom F) by A6, PARTFUN1:def 2;

          then

           A7: f is one-to-one by A1;

          ( rng f) = (B . i) by A2, A6;

          then (f " ) is Function of (B . i), (A . i) by A7, FUNCT_2: 25;

          hence thesis by A4, A6;

        end;

        then

        reconsider H as ManySortedFunction of B, A by PBOOLE:def 15;

        take H;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let H1,H2 be ManySortedFunction of B, A;

        assume that

         A8: for i be set st i in I holds (H1 . i) = ((F . i) " ) and

         A9: for i be set st i in I holds (H2 . i) = ((F . i) " );

        now

          let i be object;

          assume

           A10: i in I;

          then

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

          (H1 . i) = (f " ) by A8, A10;

          hence (H1 . i) = (H2 . i) by A9, A10;

        end;

        hence thesis by PBOOLE: 3;

      end;

    end

    theorem :: MSUALG_3:5

    

     Th5: for I be set, A,B be non-empty ManySortedSet of I, H be ManySortedFunction of A, B, H1 be ManySortedFunction of B, A st H is "1-1" "onto" & H1 = (H "" ) holds (H ** H1) = ( id B) & (H1 ** H) = ( id A)

    proof

      let I be set, A,B be non-empty ManySortedSet of I, H be ManySortedFunction of A, B, H1 be ManySortedFunction of B, A;

      assume that

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

       A2: H1 = (H "" );

       A3:

      now

        let i be set;

        assume

         A4: i in I;

        then

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

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

        i in ( dom H) by A4, PARTFUN1:def 2;

        then

         A5: h is one-to-one by A1;

        h1 = (h " ) by A1, A2, A4, Def4;

        then (h * h1) = ( id ( rng h)) by A5, FUNCT_1: 39;

        then (h * h1) = ( id (B . i)) by A1, A4;

        hence ((H ** H1) . i) = ( id (B . i)) by A4, Th2;

      end;

      for i be set st i in I holds ((H1 ** H) . i) = ( id (A . i))

      proof

        let i be set;

        assume

         A6: i in I;

        then

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

        reconsider h1 = (H1 . i) as Function of (B . i), (A . i) by A6, PBOOLE:def 15;

        i in ( dom H) by A6, PARTFUN1:def 2;

        then

         A7: h is one-to-one by A1;

        h1 = (h " ) & ( dom h) = (A . i) by A1, A2, A6, Def4, FUNCT_2:def 1;

        then (h1 * h) = ( id (A . i)) by A7, FUNCT_1: 39;

        hence thesis by A6, Th2;

      end;

      hence thesis by A3, Def1;

    end;

    registration

      let S;

      let U1 be non-empty MSAlgebra over S;

      let o;

      cluster ( Args (o,U1)) -> functional;

      coherence

      proof

        ( Args (o,U1)) = ( product (the Sorts of U1 * ( the_arity_of o))) by PRALG_2: 3;

        hence thesis;

      end;

    end

    begin

    theorem :: MSUALG_3:6

    

     Th6: for U1 be MSAlgebra over S holds for x be Function st x in ( Args (o,U1)) holds ( dom x) = ( dom ( the_arity_of o)) & for y be set st y in ( dom (the Sorts of U1 * ( the_arity_of o))) holds (x . y) in ((the Sorts of U1 * ( the_arity_of o)) . y)

    proof

      let U1 be MSAlgebra over S;

      let x be Function;

      

       A1: ( Args (o,U1)) = ( product (the Sorts of U1 * ( the_arity_of o))) by PRALG_2: 3;

      ( dom the Sorts of U1) = the carrier of S by PARTFUN1:def 2;

      then

       A2: ( rng ( the_arity_of o)) c= ( dom the Sorts of U1) by FINSEQ_1:def 4;

      assume

       A3: x in ( Args (o,U1));

      then ( dom x) = ( dom (the Sorts of U1 * ( the_arity_of o))) by A1, CARD_3: 9;

      hence thesis by A3, A1, A2, CARD_3: 9, RELAT_1: 27;

    end;

    definition

      let S;

      let U1,U2 be MSAlgebra over S;

      let o;

      let F be ManySortedFunction of U1, U2;

      let x be Element of ( Args (o,U1));

      assume that

       A1: ( Args (o,U1)) <> {} and

       A2: ( Args (o,U2)) <> {} ;

      :: MSUALG_3:def5

      func F # x -> Element of ( Args (o,U2)) equals

      : Def5: (( Frege (F * ( the_arity_of o))) . x);

      coherence

      proof

        

         A3: ( dom (the Sorts of U1 * ( the_arity_of o))) = ( dom (F * ( the_arity_of o)))

        proof

          hereby

            let e be object;

            assume

             A4: e in ( dom (the Sorts of U1 * ( the_arity_of o)));

            then (( the_arity_of o) . e) in ( dom the Sorts of U1) by FUNCT_1: 11;

            then (( the_arity_of o) . e) in the carrier of S by PARTFUN1:def 2;

            then

             A5: (( the_arity_of o) . e) in ( dom F) by PARTFUN1:def 2;

            e in ( dom ( the_arity_of o)) by A4, FUNCT_1: 11;

            then e in ( dom (F * ( the_arity_of o))) by A5, FUNCT_1: 11;

            hence e in ( dom (F * ( the_arity_of o)));

          end;

          let e be object;

          assume e in ( dom (F * ( the_arity_of o)));

          then e in ( dom (F * ( the_arity_of o)));

          then

           A6: e in ( dom ( the_arity_of o)) by FUNCT_1: 11;

          then

          reconsider f = e as Element of NAT ;

          (( the_arity_of o) . f) in the carrier of S by A6, FINSEQ_2: 11;

          then (( the_arity_of o) . e) in ( dom the Sorts of U1) by PARTFUN1:def 2;

          hence thesis by A6, FUNCT_1: 11;

        end;

        now

          let e be object;

          

           A7: ( product (the Sorts of U2 * ( the_arity_of o))) <> {} by A2, PRALG_2: 3;

          assume e in ( dom (F * ( the_arity_of o)));

          then e in ( dom (F * ( the_arity_of o)));

          then

           A8: e in ( dom ( the_arity_of o)) by FUNCT_1: 11;

          then

          reconsider f = e as Element of NAT ;

          (( the_arity_of o) . f) in the carrier of S by A8, FINSEQ_2: 11;

          then (( the_arity_of o) . e) in ( dom the Sorts of U2) by PARTFUN1:def 2;

          then

           A9: e in ( dom (the Sorts of U2 * ( the_arity_of o))) by A8, FUNCT_1: 11;

          

           A10: ((the Sorts of U2 * ( the_arity_of o)) . e) = (the Sorts of U2 . (( the_arity_of o) . e)) by A8, FUNCT_1: 13;

           A11:

          now

            assume (the Sorts of U2 . (( the_arity_of o) . e)) = {} ;

            then {} in ( rng (the Sorts of U2 * ( the_arity_of o))) by A9, A10, FUNCT_1:def 3;

            hence contradiction by A7, CARD_3: 26;

          end;

          reconsider Foe = (F . (( the_arity_of o) . e)) as Function of (the Sorts of U1 . (( the_arity_of o) . e)), (the Sorts of U2 . (( the_arity_of o) . e)) by A8, FINSEQ_2: 11, PBOOLE:def 15;

          

          thus ((the Sorts of U1 * ( the_arity_of o)) . e) = (the Sorts of U1 . (( the_arity_of o) . e)) by A8, FUNCT_1: 13

          .= ( dom Foe) by A11, FUNCT_2:def 1

          .= ( proj1 ((F * ( the_arity_of o)) . e)) by A8, FUNCT_1: 13;

        end;

        then

         A12: (the Sorts of U1 * ( the_arity_of o)) = ( doms (F * ( the_arity_of o))) by A3, FUNCT_6:def 2;

        x in ( Args (o,U1)) by A1;

        then

         A13: x in ( product (the Sorts of U1 * ( the_arity_of o))) by PRALG_2: 3;

        then

        consider f be Function such that

         A14: x = f and

         a14: ( dom f) = ( dom ( doms (F * ( the_arity_of o)))) and

         A15: for e be object st e in ( dom ( doms (F * ( the_arity_of o)))) holds (f . e) in (( doms (F * ( the_arity_of o))) . e) by A12, CARD_3:def 5;

        

         AA: ( dom ( doms (F * ( the_arity_of o)))) = ( dom (F * ( the_arity_of o))) by FUNCT_6:def 2;

        

         A16: ( dom ((F * ( the_arity_of o)) .. f)) = (( dom (F * ( the_arity_of o))) /\ ( dom f)) by PRALG_1:def 19

        .= ( dom (F * ( the_arity_of o))) by a14, AA;

        

         A17: ( rng ( the_arity_of o)) c= the carrier of S by FINSEQ_1:def 4;

        then

         A18: ( rng ( the_arity_of o)) c= ( dom the Sorts of U2) by PARTFUN1:def 2;

        

         SS: ( rng ( the_arity_of o)) c= ( dom F) by A17, PARTFUN1:def 2;

        

        then

         A19: ( dom (F * ( the_arity_of o))) = ( dom ( the_arity_of o)) by RELAT_1: 27

        .= ( dom (the Sorts of U2 * ( the_arity_of o))) by A18, RELAT_1: 27;

         A20:

        now

          let e be object;

          

           A21: ( product (the Sorts of U2 * ( the_arity_of o))) <> {} by A2, PRALG_2: 3;

          assume

           A22: e in ( dom (the Sorts of U2 * ( the_arity_of o)));

          then

           A23: e in ( dom ( the_arity_of o)) by FUNCT_1: 11;

          then

          reconsider g = (F . (( the_arity_of o) . e)) as Function of (the Sorts of U1 . (( the_arity_of o) . e)), (the Sorts of U2 . (( the_arity_of o) . e)) by FINSEQ_2: 11, PBOOLE:def 15;

          ( dom f) = ( dom ( the_arity_of o)) by A14, A1, Th6;

          then

           AC: e in ( dom f) by A23;

          then e in ( dom ( the_arity_of o)) by A1, A14, Th6;

          then e in ( dom (F * ( the_arity_of o))) by SS, RELAT_1: 27;

          then e in (( dom (F * ( the_arity_of o))) /\ ( dom f)) by AC, XBOOLE_0:def 4;

          then

           AB: e in ( dom ((F * ( the_arity_of o)) .. f)) by PRALG_1:def 19;

          reconsider r = e as Element of NAT by A23;

          g = ((F * ( the_arity_of o)) . e) by A19, A22, FUNCT_1: 12;

          then

           A24: (((F * ( the_arity_of o)) .. f) . e) = (g . (f . e)) by PRALG_1:def 19, AB;

          

           A25: ((the Sorts of U2 * ( the_arity_of o)) . e) = (the Sorts of U2 . (( the_arity_of o) . e)) by A23, FUNCT_1: 13;

           A26:

          now

            assume (the Sorts of U2 . (( the_arity_of o) . e)) = {} ;

            then {} in ( rng (the Sorts of U2 * ( the_arity_of o))) by A22, A25, FUNCT_1:def 3;

            hence contradiction by A21, CARD_3: 26;

          end;

          (( the_arity_of o) . r) in the carrier of S by A23, FINSEQ_2: 11;

          then (( the_arity_of o) . e) in ( dom the Sorts of U1) by PARTFUN1:def 2;

          then e in ( dom (the Sorts of U1 * ( the_arity_of o))) by A23, FUNCT_1: 11;

          then (f . e) in (( doms (F * ( the_arity_of o))) . e) by A12, A15;

          then (f . e) in (the Sorts of U1 . (( the_arity_of o) . e)) by A12, A23, FUNCT_1: 13;

          then (g . (f . e)) in (the Sorts of U2 . (( the_arity_of o) . e)) by A26, FUNCT_2: 5;

          hence (((F * ( the_arity_of o)) .. f) . e) in ((the Sorts of U2 * ( the_arity_of o)) . e) by A22, A24, FUNCT_1: 12;

        end;

        (( Frege (F * ( the_arity_of o))) . x) = ((F * ( the_arity_of o)) .. f) by A13, A12, A14, PRALG_2:def 2;

        then (( Frege (F * ( the_arity_of o))) . x) in ( product (the Sorts of U2 * ( the_arity_of o))) by A16, A19, A20, CARD_3: 9;

        hence thesis by PRALG_2: 3;

      end;

      correctness ;

    end

     Lm1:

    now

      let S;

      let U1,U2 be MSAlgebra over S;

      let o;

      let F be ManySortedFunction of U1, U2;

      let x be Element of ( Args (o,U1)), f,u be Function;

      assume that

       A1: f = x and

       A2: x in ( Args (o,U1)) and

       A3: u in ( Args (o,U2));

      

       A4: ( rng ( the_arity_of o)) c= the carrier of S by FINSEQ_1:def 4;

      

       A6: (F # x) = (( Frege (F * ( the_arity_of o))) . x) by A2, A3, Def5;

      

       A7: ( dom (the Sorts of U1 * ( the_arity_of o))) = ( dom (F * ( the_arity_of o)))

      proof

        hereby

          let e be object;

          assume

           A8: e in ( dom (the Sorts of U1 * ( the_arity_of o)));

          then (( the_arity_of o) . e) in ( dom the Sorts of U1) by FUNCT_1: 11;

          then (( the_arity_of o) . e) in the carrier of S by PARTFUN1:def 2;

          then

           A9: (( the_arity_of o) . e) in ( dom F) by PARTFUN1:def 2;

          e in ( dom ( the_arity_of o)) by A8, FUNCT_1: 11;

          then e in ( dom (F * ( the_arity_of o))) by A9, FUNCT_1: 11;

          hence e in ( dom (F * ( the_arity_of o)));

        end;

        let e be object;

        assume e in ( dom (F * ( the_arity_of o)));

        then

         A10: e in ( dom ( the_arity_of o)) by FUNCT_1: 11;

        then

        reconsider f = e as Element of NAT ;

        (( the_arity_of o) . f) in the carrier of S by A10, FINSEQ_2: 11;

        then (( the_arity_of o) . e) in ( dom the Sorts of U1) by PARTFUN1:def 2;

        hence thesis by A10, FUNCT_1: 11;

      end;

      

       A11: ( Args (o,U2)) = ( product (the Sorts of U2 * ( the_arity_of o))) by PRALG_2: 3;

      then

       A12: ( dom u) = ( dom (the Sorts of U2 * ( the_arity_of o))) by A3, CARD_3: 9;

      

       A13: ( Args (o,U1)) = ( product (the Sorts of U1 * ( the_arity_of o))) by PRALG_2: 3;

      

       A14: ( dom f) = ( dom ( the_arity_of o)) by A1, A2, Th6;

      ( rng ( the_arity_of o)) c= ( dom the Sorts of U2) by A4, PARTFUN1:def 2;

      then

       A15: ( dom u) = ( dom ( the_arity_of o)) by A12, RELAT_1: 27;

      set tao = ( the_arity_of o);

      now

        let e be object;

        assume e in ( dom (F * tao));

        then

         A16: e in ( dom tao) by FUNCT_1: 11;

        then

        reconsider Foe = (F . (tao . e)) as Function of (the Sorts of U1 . (tao . e)), (the Sorts of U2 . (tao . e)) by FINSEQ_2: 11, PBOOLE:def 15;

        ((the Sorts of U2 * tao) . e) in ( rng (the Sorts of U2 * tao)) by A12, A15, A16, FUNCT_1:def 3;

        then

         A17: ((the Sorts of U2 * tao) . e) <> {} by A3, A11, CARD_3: 26;

        ((the Sorts of U1 * tao) . e) = (the Sorts of U1 . (( the_arity_of o) . e)) & ((the Sorts of U2 * tao) . e) = (the Sorts of U2 . (tao . e)) by A16, FUNCT_1: 13;

        

        hence ((the Sorts of U1 * tao) . e) = ( dom Foe) by A17, FUNCT_2:def 1

        .= ( proj1 ((F * tao) . e)) by A16, FUNCT_1: 13;

      end;

      then

       A18: (the Sorts of U1 * tao) = ( doms (F * ( the_arity_of o))) by A7, FUNCT_6:def 2;

      hereby

        assume u = (F # x);

        then

         A19: u = (( Frege (F * tao)) . x) by A2, A3, Def5;

        let n;

        assume

         A20: n in ( dom f);

        then (tao . n) in the carrier of S by A14, FINSEQ_2: 11;

        then (tao . n) in ( dom F) by PARTFUN1:def 2;

        then

         A21: n in ( dom (F * ( the_arity_of o))) by A14, A20, FUNCT_1: 11;

        then n in (( dom (F * tao)) /\ ( dom f)) by A20, XBOOLE_0:def 4;

        then

         a21: n in ( dom ((F * ( the_arity_of o)) .. f)) by PRALG_1:def 19;

        

         A22: ((F * ( the_arity_of o)) . n) = (F . (( the_arity_of o) . n)) by FUNCT_1: 12, A21

        .= (F . (( the_arity_of o) /. n)) by A14, A20, PARTFUN1:def 6;

        

        thus (u . n) = (((F * ( the_arity_of o)) .. f) . n) by A1, A2, A13, A18, A19, PRALG_2:def 2

        .= ((F . (( the_arity_of o) /. n)) . (f . n)) by A22, PRALG_1:def 19, a21;

      end;

      (F # x) is Element of ( product (the Sorts of U2 * ( the_arity_of o))) by PRALG_2: 3;

      then

      reconsider g = (F # x) as Function;

      

       A23: ( rng tao) c= ( dom F) by A4, PARTFUN1:def 2;

      assume

       A24: for n st n in ( dom f) holds (u . n) = ((F . (( the_arity_of o) /. n)) . (f . n));

       A25:

      now

        let e be object;

        assume

         A26: e in ( dom f);

        then

        reconsider n = e as Nat by A14;

        (( the_arity_of o) . n) in the carrier of S by A14, A26, FINSEQ_2: 11;

        then (tao . n) in ( dom F) by PARTFUN1:def 2;

        then

         A27: n in ( dom (F * ( the_arity_of o))) by A14, A26, FUNCT_1: 11;

        then n in (( dom (F * ( the_arity_of o))) /\ ( dom f)) by A26, XBOOLE_0:def 4;

        then

         a27: n in ( dom ((F * ( the_arity_of o)) .. f)) by PRALG_1:def 19;

        

         A28: ((F * ( the_arity_of o)) . n) = (F . (( the_arity_of o) . n)) by FUNCT_1: 12, A27

        .= (F . (tao /. n)) by A14, A26, PARTFUN1:def 6;

        

        thus (u . e) = ((F . (( the_arity_of o) /. n)) . (f . n)) by A24, A26

        .= (((F * tao) .. f) . n) by a27, A28, PRALG_1:def 19

        .= (g . e) by A1, A2, A13, A18, A6, PRALG_2:def 2;

      end;

      ( dom f) = ( dom tao) by A1, A2, Th6;

      (F # x) = ((F * tao) .. f) by A1, A2, A13, A18, A6, PRALG_2:def 2;

      

      then ( dom g) = (( dom (F * tao)) /\ ( dom f)) by PRALG_1:def 19

      .= (( dom tao) /\ ( dom f)) by A23, RELAT_1: 27;

      hence u = (F # x) by A14, A15, A25, FUNCT_1: 2;

    end;

    definition

      let S;

      let U1,U2 be non-empty MSAlgebra over S;

      let o;

      let F be ManySortedFunction of U1, U2;

      let x be Element of ( Args (o,U1));

      :: original: #

      redefine

      :: MSUALG_3:def6

      func F # x means

      : Def6: for n st n in ( dom x) holds (it . n) = ((F . (( the_arity_of o) /. n)) . (x . n));

      compatibility by Lm1;

    end

    theorem :: MSUALG_3:7

    

     Th7: for S, o holds for U1 be MSAlgebra over S st ( Args (o,U1)) <> {} holds for x be Element of ( Args (o,U1)) holds x = (( id the Sorts of U1) # x)

    proof

      let S, o;

      let U1 be MSAlgebra over S;

      set F = ( id the Sorts of U1);

      assume

       A1: ( Args (o,U1)) <> {} ;

      then

      reconsider AA = ( Args (o,U1)) as non empty set;

      let x be Element of ( Args (o,U1));

      reconsider Fx = (F # x) as Element of AA;

      

       A2: ( Args (o,U1)) = ( product (the Sorts of U1 * ( the_arity_of o))) by PRALG_2: 3;

      then

      consider g be Function such that

       A3: Fx = g and ( dom g) = ( dom (the Sorts of U1 * ( the_arity_of o))) and for x be object st x in ( dom (the Sorts of U1 * ( the_arity_of o))) holds (g . x) in ((the Sorts of U1 * ( the_arity_of o)) . x) by CARD_3:def 5;

      consider f be Function such that

       A4: x = f and ( dom f) = ( dom (the Sorts of U1 * ( the_arity_of o))) and for x be object st x in ( dom (the Sorts of U1 * ( the_arity_of o))) holds (f . x) in ((the Sorts of U1 * ( the_arity_of o)) . x) by A1, A2, CARD_3:def 5;

      

       A5: ( dom f) = ( dom ( the_arity_of o)) by A4, A3, Th6;

      

       A6: for y be object st y in ( dom f) holds (f . y) = (g . y)

      proof

        let y be object;

        assume

         A7: y in ( dom f);

        then

        reconsider n = y as Nat by A5;

        set p = (( the_arity_of o) /. n);

        ( dom the Sorts of U1) = the carrier of S by PARTFUN1:def 2;

        then ( rng ( the_arity_of o)) c= ( dom the Sorts of U1) by FINSEQ_1:def 4;

        then

         A8: ( dom (the Sorts of U1 * ( the_arity_of o))) = ( dom ( the_arity_of o)) by RELAT_1: 27;

        then (f . n) in ((the Sorts of U1 * ( the_arity_of o)) . n) by A1, A4, A5, A7, Th6;

        then (f . n) in (the Sorts of U1 . (( the_arity_of o) . n)) by A5, A7, A8, FUNCT_1: 12;

        then

         A9: (f . n) in (the Sorts of U1 . p) by A5, A7, PARTFUN1:def 6;

        

         A10: (F . p) = ( id (the Sorts of U1 . p)) by Def1;

        (g . n) = ((F . (( the_arity_of o) /. n)) . (f . n)) by A4, A3, A7, Lm1;

        hence thesis by A10, A9, FUNCT_1: 18;

      end;

      ( dom g) = ( dom ( the_arity_of o)) by A3, Th6;

      hence thesis by A4, A3, A6, Th6, FUNCT_1: 2;

    end;

    theorem :: MSUALG_3:8

    

     Th8: for U1,U2,U3 be non-empty MSAlgebra over S holds for H1 be ManySortedFunction of U1, U2, H2 be ManySortedFunction of U2, U3, x be Element of ( Args (o,U1)) holds ((H2 ** H1) # x) = (H2 # (H1 # x))

    proof

      let U1,U2,U3 be non-empty MSAlgebra over S;

      let H1 be ManySortedFunction of U1, U2, H2 be ManySortedFunction of U2, U3;

      let x be Element of ( Args (o,U1));

      

       A1: ( dom x) = ( dom ( the_arity_of o)) by Th6;

      

       A2: ( dom (H1 # x)) = ( dom ( the_arity_of o)) by Th6;

      

       A3: for y be object st y in ( dom ( the_arity_of o)) holds (((H2 ** H1) # x) . y) = ((H2 # (H1 # x)) . y)

      proof

        ( rng ( the_arity_of o)) c= the carrier of S by FINSEQ_1:def 4;

        then ( rng ( the_arity_of o)) c= ( dom the Sorts of U1) by PARTFUN1:def 2;

        then

         A4: ( dom (the Sorts of U1 * ( the_arity_of o))) = ( dom ( the_arity_of o)) by RELAT_1: 27;

        let y be object;

        assume

         A5: y in ( dom ( the_arity_of o));

        then

        reconsider n = y as Nat;

        set F = (H2 ** H1), p = (( the_arity_of o) /. n);

        

         A6: ((F # x) . n) = ((F . p) . (x . n)) by A1, A5, Def6;

        p = (( the_arity_of o) . n) by A5, PARTFUN1:def 6;

        then

         A7: ((the Sorts of U1 * ( the_arity_of o)) . n) = (the Sorts of U1 . p) by A5, A4, FUNCT_1: 12;

        

         A8: (F . p) = ((H2 . p) * (H1 . p)) by Th2;

        

         A9: ( dom (H1 . p)) = (the Sorts of U1 . p) by FUNCT_2:def 1;

        then ( dom ((H2 . p) * (H1 . p))) = ( dom (H1 . p)) by FUNCT_2:def 1;

        

        hence ((F # x) . y) = ((H2 . p) . ((H1 . p) . (x . n))) by A5, A6, A4, A9, A7, A8, Th6, FUNCT_1: 12

        .= ((H2 . p) . ((H1 # x) . n)) by A1, A5, Def6

        .= ((H2 # (H1 # x)) . y) by A2, A5, Def6;

      end;

      ( dom ((H2 ** H1) # x)) = ( dom ( the_arity_of o)) & ( dom (H2 # (H1 # x))) = ( dom ( the_arity_of o)) by Th6;

      hence thesis by A3, FUNCT_1: 2;

    end;

    definition

      let S;

      let U1,U2 be MSAlgebra over S;

      let F be ManySortedFunction of U1, U2;

      :: MSUALG_3:def7

      pred F is_homomorphism U1,U2 means for o be OperSymbol of S st ( Args (o,U1)) <> {} holds for x be Element of ( Args (o,U1)) holds ((F . ( the_result_sort_of o)) . (( Den (o,U1)) . x)) = (( Den (o,U2)) . (F # x));

    end

    theorem :: MSUALG_3:9

    

     Th9: for U1 be MSAlgebra over S holds ( id the Sorts of U1) is_homomorphism (U1,U1)

    proof

      let U1 be MSAlgebra over S;

      set F = ( id the Sorts of U1);

      let o be OperSymbol of S;

      assume

       A1: ( Args (o,U1)) <> {} ;

      let x be Element of ( Args (o,U1));

      

       A2: (F # x) = x by A1, Th7;

      set r = ( the_result_sort_of o);

      

       A3: (F . r) = ( id (the Sorts of U1 . r)) by Def1;

      ( rng the ResultSort of S) c= the carrier of S by RELAT_1:def 19;

      then ( rng the ResultSort of S) c= ( dom the Sorts of U1) by PARTFUN1:def 2;

      then

       A4: ( Result (o,U1)) = ((the Sorts of U1 * the ResultSort of S) . o) & ( dom (the Sorts of U1 * the ResultSort of S)) = ( dom the ResultSort of S) by MSUALG_1:def 5, RELAT_1: 27;

      o in the carrier' of S;

      then o in ( dom the ResultSort of S) by FUNCT_2:def 1;

      

      then

       A5: ( Result (o,U1)) = (the Sorts of U1 . (the ResultSort of S . o)) by A4, FUNCT_1: 12

      .= (the Sorts of U1 . r) by MSUALG_1:def 2;

      per cases ;

        suppose ( Result (o,U1)) <> {} ;

        then ( dom ( Den (o,U1))) = ( Args (o,U1)) by FUNCT_2:def 1;

        then ( rng ( Den (o,U1))) c= ( Result (o,U1)) & (( Den (o,U1)) . x) in ( rng ( Den (o,U1))) by A1, FUNCT_1:def 3, RELAT_1:def 19;

        hence thesis by A2, A3, A5, FUNCT_1: 18;

      end;

        suppose

         A6: ( Result (o,U1)) = {} ;

        then ( dom ( Den (o,U1))) = {} ;

        then

         A7: (( Den (o,U1)) . x) = {} by FUNCT_1:def 2;

        ( dom (F . r)) = {} by A5, A6;

        then ((F . r) . {} ) = {} by FUNCT_1:def 2;

        hence thesis by A1, A7, Th7;

      end;

    end;

    theorem :: MSUALG_3:10

    

     Th10: for U1,U2,U3 be non-empty MSAlgebra over S holds for H1 be ManySortedFunction of U1, U2, H2 be ManySortedFunction of U2, U3 st H1 is_homomorphism (U1,U2) & H2 is_homomorphism (U2,U3) holds (H2 ** H1) is_homomorphism (U1,U3)

    proof

      let U1,U2,U3 be non-empty MSAlgebra over S;

      let H1 be ManySortedFunction of U1, U2, H2 be ManySortedFunction of U2, U3;

      assume that

       A1: H1 is_homomorphism (U1,U2) and

       A2: H2 is_homomorphism (U2,U3);

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

      let x be Element of ( Args (o,U1));

      set F = (H2 ** H1), r = ( the_result_sort_of o);

      ((H1 . r) . (( Den (o,U1)) . x)) = (( Den (o,U2)) . (H1 # x)) by A1;

      then

       A3: ((H2 . r) . ((H1 . r) . (( Den (o,U1)) . x))) = (( Den (o,U3)) . (H2 # (H1 # x))) by A2;

      

       A4: (F . r) = ((H2 . r) * (H1 . r)) & ( dom (F . r)) = (the Sorts of U1 . r) by Th2, FUNCT_2:def 1;

      ( rng the ResultSort of S) c= the carrier of S by RELAT_1:def 19;

      then ( rng the ResultSort of S) c= ( dom the Sorts of U1) by PARTFUN1:def 2;

      then

       A5: ( Result (o,U1)) = ((the Sorts of U1 * the ResultSort of S) . o) & ( dom (the Sorts of U1 * the ResultSort of S)) = ( dom the ResultSort of S) by MSUALG_1:def 5, RELAT_1: 27;

      o in the carrier' of S;

      then o in ( dom the ResultSort of S) by FUNCT_2:def 1;

      

      then ( Result (o,U1)) = (the Sorts of U1 . (the ResultSort of S . o)) by A5, FUNCT_1: 12

      .= (the Sorts of U1 . r) by MSUALG_1:def 2;

      then ((F . r) . (( Den (o,U1)) . x)) = (( Den (o,U3)) . (H2 # (H1 # x))) by A3, A4, FUNCT_1: 12;

      hence ((F . r) . (( Den (o,U1)) . x)) = (( Den (o,U3)) . (F # x)) by Th8;

    end;

    definition

      let S;

      let U1,U2 be MSAlgebra over S;

      let F be ManySortedFunction of U1, U2;

      :: MSUALG_3:def8

      pred F is_epimorphism U1,U2 means F is_homomorphism (U1,U2) & F is "onto";

    end

    theorem :: MSUALG_3:11

    

     Th11: for U1,U2,U3 be non-empty MSAlgebra over S holds for F be ManySortedFunction of U1, U2, G be ManySortedFunction of U2, U3 st F is_epimorphism (U1,U2) & G is_epimorphism (U2,U3) holds (G ** F) is_epimorphism (U1,U3)

    proof

      let U1,U2,U3 be non-empty MSAlgebra over S;

      let F be ManySortedFunction of U1, U2, G be ManySortedFunction of U2, U3;

      assume that

       A1: F is_epimorphism (U1,U2) and

       A2: G is_epimorphism (U2,U3);

      

       A3: G is "onto" by A2;

      

       A4: F is "onto" by A1;

      for i be set st i in the carrier of S holds ( rng ((G ** F) . i)) = (the Sorts of U3 . i)

      proof

        let i be set;

        assume

         A5: i in the carrier of S;

        then

        reconsider f = (F . i) as Function of (the Sorts of U1 . i), (the Sorts of U2 . i) by PBOOLE:def 15;

        reconsider g = (G . i) as Function of (the Sorts of U2 . i), (the Sorts of U3 . i) by A5, PBOOLE:def 15;

        ( rng f) = (the Sorts of U2 . i) by A4, A5;

        then

         A6: ( dom g) = ( rng f) by A5, FUNCT_2:def 1;

        ( rng g) = (the Sorts of U3 . i) by A3, A5;

        then ( rng (g * f)) = (the Sorts of U3 . i) by A6, RELAT_1: 28;

        hence thesis by A5, Th2;

      end;

      then

       A7: (G ** F) is "onto";

      F is_homomorphism (U1,U2) & G is_homomorphism (U2,U3) by A1, A2;

      then (G ** F) is_homomorphism (U1,U3) by Th10;

      hence thesis by A7;

    end;

    definition

      let S;

      let U1,U2 be MSAlgebra over S;

      let F be ManySortedFunction of U1, U2;

      :: MSUALG_3:def9

      pred F is_monomorphism U1,U2 means F is_homomorphism (U1,U2) & F is "1-1";

    end

    theorem :: MSUALG_3:12

    

     Th12: for U1,U2,U3 be non-empty MSAlgebra over S holds for F be ManySortedFunction of U1, U2, G be ManySortedFunction of U2, U3 st F is_monomorphism (U1,U2) & G is_monomorphism (U2,U3) holds (G ** F) is_monomorphism (U1,U3)

    proof

      let U1,U2,U3 be non-empty MSAlgebra over S;

      let F be ManySortedFunction of U1, U2, G be ManySortedFunction of U2, U3;

      assume that

       A1: F is_monomorphism (U1,U2) and

       A2: G is_monomorphism (U2,U3);

      

       A3: G is "1-1" by A2;

      

       A4: F is "1-1" by A1;

      for i be set, h be Function st i in ( dom (G ** F)) & ((G ** F) . i) = h holds h is one-to-one

      proof

        let i be set, h be Function;

        assume that

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

         A6: ((G ** F) . i) = h;

        

         A7: i in the carrier of S by A5, PARTFUN1:def 2;

        then

        reconsider g = (G . i) as Function of (the Sorts of U2 . i), (the Sorts of U3 . i) by PBOOLE:def 15;

        reconsider f = (F . i) as Function of (the Sorts of U1 . i), (the Sorts of U2 . i) by A7, PBOOLE:def 15;

        i in ( dom G) by A7, PARTFUN1:def 2;

        then

         A8: g is one-to-one by A3;

        i in ( dom F) by A7, PARTFUN1:def 2;

        then f is one-to-one by A4;

        then (g * f) is one-to-one by A8;

        hence thesis by A6, A7, Th2;

      end;

      then

       A9: (G ** F) is "1-1";

      F is_homomorphism (U1,U2) & G is_homomorphism (U2,U3) by A1, A2;

      then (G ** F) is_homomorphism (U1,U3) by Th10;

      hence thesis by A9;

    end;

    definition

      let S;

      let U1,U2 be MSAlgebra over S;

      let F be ManySortedFunction of U1, U2;

      :: MSUALG_3:def10

      pred F is_isomorphism U1,U2 means F is_epimorphism (U1,U2) & F is_monomorphism (U1,U2);

    end

    theorem :: MSUALG_3:13

    

     Th13: for F be ManySortedFunction of U1, U2 holds F is_isomorphism (U1,U2) iff F is_homomorphism (U1,U2) & F is "onto" & F is "1-1"

    proof

      let F be ManySortedFunction of U1, U2;

      thus F is_isomorphism (U1,U2) implies F is_homomorphism (U1,U2) & F is "onto" & F is "1-1"

      proof

        assume F is_isomorphism (U1,U2);

        then F is_epimorphism (U1,U2) & F is_monomorphism (U1,U2);

        hence thesis;

      end;

      assume F is_homomorphism (U1,U2) & F is "onto" & F is "1-1";

      then F is_epimorphism (U1,U2) & F is_monomorphism (U1,U2);

      hence thesis;

    end;

    

     Lm2: for U1,U2 be non-empty MSAlgebra over S holds for H be ManySortedFunction of U1, U2 st H is_isomorphism (U1,U2) holds (H "" ) is_homomorphism (U2,U1)

    proof

      let U1,U2 be non-empty MSAlgebra over S;

      let H be ManySortedFunction of U1, U2;

      set F = (H "" );

      assume

       A1: H is_isomorphism (U1,U2);

      then

       A2: H is "onto" by Th13;

      

       A3: H is "1-1" by A1, Th13;

      

       A4: H is_homomorphism (U1,U2) by A1, Th13;

      for o be OperSymbol of S st ( Args (o,U2)) <> {} holds for x be Element of ( Args (o,U2)) holds ((F . ( the_result_sort_of o)) . (( Den (o,U2)) . x)) = (( Den (o,U1)) . (F # x))

      proof

        let o be OperSymbol of S such that ( Args (o,U2)) <> {} ;

        let x be Element of ( Args (o,U2));

        set r = ( the_result_sort_of o);

        deffunc G( object) = ((F # x) . $1);

        consider f be Function such that

         A5: ( dom f) = ( dom ( the_arity_of o)) & for n be object st n in ( dom ( the_arity_of o)) holds (f . n) = G(n) from FUNCT_1:sch 3;

        

         A6: ( dom (F # x)) = ( dom ( the_arity_of o)) by Th6;

        then

         A7: f = (F # x) by A5, FUNCT_1: 2;

        r in the carrier of S;

        then r in ( dom H) by PARTFUN1:def 2;

        then

         A8: (H . r) is one-to-one by A3;

        ( dom (H . r)) = (the Sorts of U1 . r) & (F . r) = ((H . r) " ) by A2, A3, Def4, FUNCT_2:def 1;

        then

         A9: ((F . r) * (H . r)) = ( id (the Sorts of U1 . r)) by A8, FUNCT_1: 39;

        

         A10: ( dom the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;

        then

         A11: ( dom (the Sorts of U1 * the ResultSort of S)) = ( dom the ResultSort of S) by PARTFUN1:def 2;

        

         A12: ( Result (o,U1)) = ((the Sorts of U1 * the ResultSort of S) . o) by MSUALG_1:def 5

        .= (the Sorts of U1 . (the ResultSort of S . o)) by A10, A11, FUNCT_1: 12

        .= (the Sorts of U1 . r) by MSUALG_1:def 2;

        reconsider f as Element of ( Args (o,U1)) by A5, A6, FUNCT_1: 2;

        

         A13: ( dom ((F . r) * (H . r))) = (the Sorts of U1 . r) by FUNCT_2:def 1;

        ((H . r) . (( Den (o,U1)) . f)) = (( Den (o,U2)) . (H # (F # x))) by A4, A7

        .= (( Den (o,U2)) . ((H ** F) # x)) by Th8

        .= (( Den (o,U2)) . (( id the Sorts of U2) # x)) by A2, A3, Th5

        .= (( Den (o,U2)) . x) by Th7;

        

        then ((F . r) . (( Den (o,U2)) . x)) = (((F . r) * (H . r)) . (( Den (o,U1)) . (F # x))) by A7, A13, A12, FUNCT_1: 12

        .= (( Den (o,U1)) . (F # x)) by A12, A9;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: MSUALG_3:14

    

     Th14: for U1,U2 be non-empty MSAlgebra over S holds for H be ManySortedFunction of U1, U2, H1 be ManySortedFunction of U2, U1 st H is_isomorphism (U1,U2) & H1 = (H "" ) holds H1 is_isomorphism (U2,U1)

    proof

      let U1,U2 be non-empty MSAlgebra over S;

      let H be ManySortedFunction of U1, U2, H1 be ManySortedFunction of U2, U1;

      assume that

       A1: H is_isomorphism (U1,U2) and

       A2: H1 = (H "" );

      

       A3: H1 is_homomorphism (U2,U1) by A1, A2, Lm2;

      H is_monomorphism (U1,U2) by A1;

      then

       A4: H is "1-1";

      H is_epimorphism (U1,U2) by A1;

      then

       A5: H is "onto";

      for i be set, g be Function st i in ( dom H1) & g = (H1 . i) holds g is one-to-one

      proof

        let i be set;

        let g be Function;

        assume that

         A6: i in ( dom H1) and

         A7: g = (H1 . i);

        

         A8: i in the carrier of S by A6, PARTFUN1:def 2;

        then

        reconsider f = (H . i) as Function of (the Sorts of U1 . i), (the Sorts of U2 . i) by PBOOLE:def 15;

        i in ( dom H) by A8, PARTFUN1:def 2;

        then f is one-to-one by A4;

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

        hence thesis by A2, A4, A5, A7, A8, Def4;

      end;

      then H1 is "1-1";

      then

       A9: H1 is_monomorphism (U2,U1) by A3;

      for i be set st i in the carrier of S holds ( rng (H1 . i)) = (the Sorts of U1 . i)

      proof

        let i be set;

        assume

         A10: i in the carrier of S;

        then

        reconsider f = (H . i) as Function of (the Sorts of U1 . i), (the Sorts of U2 . i) by PBOOLE:def 15;

        i in ( dom H) by A10, PARTFUN1:def 2;

        then f is one-to-one by A4;

        then ( rng (f " )) = ( dom f) by FUNCT_1: 33;

        then ( rng (f " )) = (the Sorts of U1 . i) by A10, FUNCT_2:def 1;

        hence thesis by A2, A4, A5, A10, Def4;

      end;

      then H1 is "onto";

      then H1 is_epimorphism (U2,U1) by A3;

      hence thesis by A9;

    end;

    theorem :: MSUALG_3:15

    

     Th15: for U1,U2,U3 be non-empty MSAlgebra over S holds for H be ManySortedFunction of U1, U2, H1 be ManySortedFunction of U2, U3 st H is_isomorphism (U1,U2) & H1 is_isomorphism (U2,U3) holds (H1 ** H) is_isomorphism (U1,U3) by Th11, Th12;

    definition

      let S;

      let U1,U2 be MSAlgebra over S;

      :: MSUALG_3:def11

      pred U1,U2 are_isomorphic means ex F be ManySortedFunction of U1, U2 st F is_isomorphism (U1,U2);

    end

    theorem :: MSUALG_3:16

    

     Th16: for U1 be MSAlgebra over S holds ( id the Sorts of U1) is_isomorphism (U1,U1) & (U1,U1) are_isomorphic

    proof

      let U1 be MSAlgebra over S;

      

       A1: ( id the Sorts of U1) is_homomorphism (U1,U1) by Th9;

      for i be set, f be Function st i in ( dom ( id the Sorts of U1)) & (( id the Sorts of U1) . i) = f holds f is one-to-one

      proof

        let i be set, f be Function;

        assume that

         A2: i in ( dom ( id the Sorts of U1)) and

         A3: (( id the Sorts of U1) . i) = f;

        i in the carrier of S by A2, PARTFUN1:def 2;

        then f = ( id (the Sorts of U1 . i)) by A3, Def1;

        hence thesis;

      end;

      then ( id the Sorts of U1) is "1-1";

      then

       A4: ( id the Sorts of U1) is_monomorphism (U1,U1) by A1;

      for i be set st i in the carrier of S holds ( rng (( id the Sorts of U1) . i)) = (the Sorts of U1 . i)

      proof

        let i be set;

        assume i in the carrier of S;

        then (( id the Sorts of U1) . i) = ( id (the Sorts of U1 . i)) by Def1;

        hence thesis;

      end;

      then ( id the Sorts of U1) is "onto";

      then

       A5: ( id the Sorts of U1) is_epimorphism (U1,U1) by A1;

      hence ( id the Sorts of U1) is_isomorphism (U1,U1) by A4;

      take ( id the Sorts of U1);

      thus thesis by A4, A5;

    end;

    definition

      let S;

      let U1,U2 be MSAlgebra over S;

      :: original: are_isomorphic

      redefine

      pred U1,U2 are_isomorphic ;

      reflexivity by Th16;

    end

    theorem :: MSUALG_3:17

    for U1,U2 be non-empty MSAlgebra over S holds (U1,U2) are_isomorphic implies (U2,U1) are_isomorphic

    proof

      let U1,U2 be non-empty MSAlgebra over S;

      assume (U1,U2) are_isomorphic ;

      then

      consider F be ManySortedFunction of U1, U2 such that

       A1: F is_isomorphism (U1,U2);

      reconsider G = (F "" ) as ManySortedFunction of U2, U1;

      G is_isomorphism (U2,U1) by A1, Th14;

      hence thesis;

    end;

    theorem :: MSUALG_3:18

    for U1,U2,U3 be non-empty MSAlgebra over S holds (U1,U2) are_isomorphic & (U2,U3) are_isomorphic implies (U1,U3) are_isomorphic

    proof

      let U1,U2,U3 be non-empty MSAlgebra over S;

      assume that

       A1: (U1,U2) are_isomorphic and

       A2: (U2,U3) are_isomorphic ;

      consider F be ManySortedFunction of U1, U2 such that

       A3: F is_isomorphism (U1,U2) by A1;

      consider G be ManySortedFunction of U2, U3 such that

       A4: G is_isomorphism (U2,U3) by A2;

      reconsider H = (G ** F) as ManySortedFunction of U1, U3;

      H is_isomorphism (U1,U3) by A3, A4, Th15;

      hence thesis;

    end;

    definition

      let S;

      let U1,U2 be non-empty MSAlgebra over S;

      let F be ManySortedFunction of U1, U2;

      assume

       A1: F is_homomorphism (U1,U2);

      :: MSUALG_3:def12

      func Image F -> strict non-empty MSSubAlgebra of U2 means

      : Def12: the Sorts of it = (F .:.: the Sorts of U1);

      existence

      proof

        set u2 = (F .:.: the Sorts of U1);

         A2:

        now

          let i be object;

          reconsider f = (F . i) as Function;

          assume

           A3: i in the carrier of S;

          then

           A4: (u2 . i) = (f .: (the Sorts of U1 . i)) by PBOOLE:def 20;

          reconsider f as Function of (the Sorts of U1 . i), (the Sorts of U2 . i) by A3, PBOOLE:def 15;

          ( dom f) = (the Sorts of U1 . i) by A3, FUNCT_2:def 1;

          hence (u2 . i) is non empty by A3, A4;

        end;

        now

          let i be object;

          reconsider f = (F . i) as Function;

          assume

           A5: i in the carrier of S;

          then

           A6: (u2 . i) = (f .: (the Sorts of U1 . i)) by PBOOLE:def 20;

          reconsider f as Function of (the Sorts of U1 . i), (the Sorts of U2 . i) by A5, PBOOLE:def 15;

          

           A7: ( rng f) c= (the Sorts of U2 . i) by RELAT_1:def 19;

          ( dom f) = (the Sorts of U1 . i) by A5, FUNCT_2:def 1;

          hence (u2 . i) c= (the Sorts of U2 . i) by A6, A7, RELAT_1: 113;

        end;

        then u2 c= the Sorts of U2 by PBOOLE:def 2;

        then

        reconsider u2 as non-empty MSSubset of U2 by A2, PBOOLE:def 13, PBOOLE:def 18;

        set M = ( GenMSAlg u2);

        reconsider M9 = MSAlgebra (# u2, ( Opers (U2,u2)) qua ManySortedFunction of ((u2 # ) * the Arity of S), (u2 * the ResultSort of S) #) as non-empty MSAlgebra over S by MSUALG_1:def 3;

        take M;

        u2 is opers_closed

        proof

          let o be OperSymbol of S;

          thus ( rng (( Den (o,U2)) | (((u2 # ) * the Arity of S) . o))) c= ((u2 * the ResultSort of S) . o)

          proof

            let x be object;

            set D = ( Den (o,U2)), X = (((u2 # ) * the Arity of S) . o), ao = ( the_arity_of o), ro = ( the_result_sort_of o), ut = (u2 * ao), S1 = the Sorts of U1;

            

             A8: ( rng ao) c= the carrier of S by FINSEQ_1:def 4;

            

             A9: ( dom the Arity of S) = the carrier' of S by FUNCT_2:def 1;

            then ( dom ((u2 # ) * the Arity of S)) = ( dom the Arity of S) by PARTFUN1:def 2;

            

            then

             A10: X = ((u2 # ) . (the Arity of S . o)) by A9, FUNCT_1: 12

            .= ((u2 # ) . ao) by MSUALG_1:def 1

            .= ( product (u2 * ao)) by FINSEQ_2:def 5;

            assume x in ( rng (D | X));

            then

            consider a be object such that

             A11: a in ( dom (D | X)) and

             A12: x = ((D | X) . a) by FUNCT_1:def 3;

            

             A13: x = (D . a) by A11, A12, FUNCT_1: 47;

            ( dom (D | X)) c= ( dom D) by RELAT_1: 60;

            then

            reconsider a as Element of ( Args (o,U2)) by A11, FUNCT_2:def 1;

            defpred P[ object, object] means for s be SortSymbol of S st s = (ao . $1) holds $2 in (S1 . s) & (a . $1) = ((F . s) . $2);

            

             A14: ( dom (D | X)) c= X by RELAT_1: 58;

            then

             A15: ( dom a) = ( dom ut) by A11, A10, CARD_3: 9;

            

             A16: ( dom u2) = the carrier of S by PARTFUN1:def 2;

            

             A17: for y be object st y in ( dom a) holds ex i be object st P[y, i]

            proof

              let y be object;

              assume

               A18: y in ( dom a);

              then

               A19: (a . y) in (ut . y) by A11, A14, A10, A15, CARD_3: 9;

              ( dom (u2 * ao)) = ( dom ao) by A16, A8, RELAT_1: 27;

              then (ao . y) in ( rng ao) by A15, A18, FUNCT_1:def 3;

              then

              reconsider s = (ao . y) as SortSymbol of S by A8;

              

               A20: ( dom (F . s)) = (S1 . s) by FUNCT_2:def 1;

              (ut . y) = (u2 . (ao . y)) by A15, A18, FUNCT_1: 12

              .= ((F . s) .: (S1 . s)) by PBOOLE:def 20

              .= ( rng (F . s)) by A20, RELAT_1: 113;

              then

              consider i be object such that

               A21: i in (S1 . s) & (a . y) = ((F . s) . i) by A20, A19, FUNCT_1:def 3;

              take i;

              thus thesis by A21;

            end;

            consider f be Function such that

             A22: ( dom f) = ( dom a) & for y be object st y in ( dom a) holds P[y, (f . y)] from CLASSES1:sch 1( A17);

            ( dom S1) = the carrier of S by PARTFUN1:def 2;

            then

             A23: ( dom (S1 * ao)) = ( dom ao) by A8, RELAT_1: 27;

            

             A24: ( dom f) = ( dom ao) by A15, A16, A8, A22, RELAT_1: 27;

            

             A25: for y be object st y in ( dom (S1 * ao)) holds (f . y) in ((S1 * ao) . y)

            proof

              let y be object;

              assume

               A26: y in ( dom (S1 * ao));

              then (ao . y) in ( rng ao) by A23, FUNCT_1:def 3;

              then

              reconsider s = (ao . y) as SortSymbol of S by A8;

              (f . y) in (S1 . s) by A22, A24, A23, A26;

              hence thesis by A26, FUNCT_1: 12;

            end;

            ( Args (o,U1)) = ( product (S1 * ao)) by PRALG_2: 3;

            then

            reconsider a1 = f as Element of ( Args (o,U1)) by A24, A23, A25, CARD_3: 9;

            

             A27: ( dom a1) = ( dom ao) by Th6;

             A28:

            now

              let y be object;

              assume

               A29: y in ( dom ao);

              then

              reconsider n = y as Nat;

              (ao . y) in ( rng ao) by A29, FUNCT_1:def 3;

              then

              reconsider s = (ao . y) as SortSymbol of S by A8;

              ((F # a1) . n) = ((F . (ao /. n)) . (a1 . n)) by A27, A29, Def6

              .= ((F . s) . (a1 . n)) by A29, PARTFUN1:def 6;

              hence ((F # a1) . y) = (a . y) by A22, A27, A29;

            end;

            ( dom (F # a1)) = ( dom ao) & ( dom a) = ( dom ao) by Th6;

            then (F # a1) = a by A28, FUNCT_1: 2;

            then

             A30: ((F . ro) . (( Den (o,U1)) . a1)) = x by A1, A13;

            reconsider g = (F . ro) as Function;

            

             A31: ( dom (F . ro)) = (S1 . ro) by FUNCT_2:def 1;

            

             A32: ( dom the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;

            then

             A33: ( dom (S1 * the ResultSort of S)) = ( dom the ResultSort of S) by PARTFUN1:def 2;

            ( Result (o,U1)) = ((S1 * the ResultSort of S) . o) by MSUALG_1:def 5

            .= (S1 . (the ResultSort of S . o)) by A32, A33, FUNCT_1: 12

            .= (S1 . ro) by MSUALG_1:def 2;

            then (( Den (o,U1)) . a1) in (S1 . ro);

            then

             A34: (( Den (o,U1)) . a1) in ( dom (F . ro)) by FUNCT_2:def 1;

            ( dom (u2 * the ResultSort of S)) = ( dom the ResultSort of S) by A32, PARTFUN1:def 2;

            

            then ((u2 * the ResultSort of S) . o) = (u2 . (the ResultSort of S . o)) by A32, FUNCT_1: 12

            .= (u2 . ro) by MSUALG_1:def 2

            .= (g .: (S1 . ro)) by PBOOLE:def 20

            .= ( rng g) by A31, RELAT_1: 113;

            hence thesis by A30, A34, FUNCT_1:def 3;

          end;

        end;

        then for B be MSSubset of U2 st B = the Sorts of M9 holds B is opers_closed & the Charact of M9 = ( Opers (U2,B));

        then

         A35: M9 is MSSubAlgebra of U2 by MSUALG_2:def 9;

        u2 is MSSubset of M9 by PBOOLE:def 18;

        then M is MSSubAlgebra of M9 by A35, MSUALG_2:def 17;

        then the Sorts of M is MSSubset of M9 by MSUALG_2:def 9;

        then

         A36: the Sorts of M c= u2 by PBOOLE:def 18;

        u2 is MSSubset of M by MSUALG_2:def 17;

        then u2 c= the Sorts of M by PBOOLE:def 18;

        hence thesis by A36, PBOOLE: 146;

      end;

      uniqueness by MSUALG_2: 9;

    end

    theorem :: MSUALG_3:19

    for U1 be non-empty MSAlgebra over S, U2 be non-empty MSAlgebra over S, F be ManySortedFunction of U1, U2 st F is_homomorphism (U1,U2) holds F is_epimorphism (U1,U2) iff ( Image F) = the MSAlgebra of U2

    proof

      let U1 be non-empty MSAlgebra over S;

      let U2 be non-empty MSAlgebra over S, F be ManySortedFunction of U1, U2;

      set FF = (F .:.: the Sorts of U1);

      assume

       A1: F is_homomorphism (U1,U2);

      thus F is_epimorphism (U1,U2) implies ( Image F) = the MSAlgebra of U2

      proof

        assume F is_epimorphism (U1,U2);

        then

         A2: F is "onto";

        now

          let i be object;

          assume

           A3: i in the carrier of S;

          then

          reconsider f = (F . i) as Function of (the Sorts of U1 . i), (the Sorts of U2 . i) by PBOOLE:def 15;

          

           A4: ( rng f) = (the Sorts of U2 . i) by A2, A3;

          reconsider f as Function;

          (FF . i) = (f .: (the Sorts of U1 . i)) & ( dom f) = (the Sorts of U1 . i) by A3, FUNCT_2:def 1, PBOOLE:def 20;

          hence (FF . i) = (the Sorts of U2 . i) by A4, RELAT_1: 113;

        end;

        then

         A5: FF = the Sorts of U2 by PBOOLE: 3;

         the MSAlgebra of U2 is strict MSSubAlgebra of U2 by MSUALG_2: 5;

        hence thesis by A1, A5, Def12;

      end;

      assume ( Image F) = the MSAlgebra of U2;

      then

       A6: FF = the Sorts of U2 by A1, Def12;

      for i be set st i in the carrier of S holds ( rng (F . i)) = (the Sorts of U2 . i)

      proof

        let i be set;

        assume i in the carrier of S;

        then

        reconsider i as Element of S;

        reconsider f = (F . i) as Function of (the Sorts of U1 . i), (the Sorts of U2 . i);

        (f .: (the Sorts of U1 . i)) = (the Sorts of U2 . i) & ( dom f) = (the Sorts of U1 . i) by A6, FUNCT_2:def 1, PBOOLE:def 20;

        hence thesis by RELAT_1: 113;

      end;

      then F is "onto";

      hence thesis by A1;

    end;

    

     Lm3: for U1,U2 be non-empty MSAlgebra over S holds for F be ManySortedFunction of U1, U2 st F is_homomorphism (U1,U2) holds F is ManySortedFunction of U1, ( Image F)

    proof

      let U1,U2 be non-empty MSAlgebra over S;

      let F be ManySortedFunction of U1, U2;

      assume

       A1: F is_homomorphism (U1,U2);

      for i be object st i in the carrier of S holds (F . i) is Function of (the Sorts of U1 . i), (the Sorts of ( Image F) . i)

      proof

        let i be object;

        assume

         A2: i in the carrier of S;

        then

        reconsider f = (F . i) as Function of (the Sorts of U1 . i), (the Sorts of U2 . i) by PBOOLE:def 15;

        

         A3: ( dom f) = (the Sorts of U1 . i) by A2, FUNCT_2:def 1;

        the Sorts of ( Image F) = (F .:.: the Sorts of U1) by A1, Def12;

        

        then (the Sorts of ( Image F) . i) = (f .: (the Sorts of U1 . i)) by A2, PBOOLE:def 20

        .= ( rng f) by A3, RELAT_1: 113;

        hence thesis by A3, FUNCT_2: 1;

      end;

      hence thesis by PBOOLE:def 15;

    end;

    theorem :: MSUALG_3:20

    

     Th20: for U1,U2 be non-empty MSAlgebra over S holds for F be ManySortedFunction of U1, U2, G be ManySortedFunction of U1, ( Image F) st F = G & F is_homomorphism (U1,U2) holds G is_epimorphism (U1,( Image F))

    proof

      let U1,U2 be non-empty MSAlgebra over S;

      let F be ManySortedFunction of U1, U2, G be ManySortedFunction of U1, ( Image F);

      assume that

       A1: F = G and

       A2: F is_homomorphism (U1,U2);

      for o be OperSymbol of S st ( Args (o,U1)) <> {} holds for x be Element of ( Args (o,U1)) holds ((G . ( the_result_sort_of o)) . (( Den (o,U1)) . x)) = (( Den (o,( Image F))) . (G # x))

      proof

        set IF = ( Image F);

        reconsider SIF = the Sorts of IF as non-empty MSSubset of U2 by MSUALG_2:def 9;

        reconsider G1 = G as ManySortedFunction of U1, U2 by A1;

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

        let x be Element of ( Args (o,U1));

        set SIFo = (SIF * ( the_arity_of o)), Uo = (the Sorts of U2 * ( the_arity_of o)), ao = ( the_arity_of o);

        

         A3: ( dom ( Den (o,U2))) = ( Args (o,U2)) by FUNCT_2:def 1;

        

         A4: ( rng ao) c= the carrier of S by FINSEQ_1:def 4;

        then ( rng ao) c= ( dom SIF) by PARTFUN1:def 2;

        then

         A5: ( dom SIFo) = ( dom ao) by RELAT_1: 27;

        ( rng ao) c= ( dom the Sorts of U2) by A4, PARTFUN1:def 2;

        then

         A6: ( dom SIFo) = ( dom Uo) by A5, RELAT_1: 27;

        

         A7: for x be object st x in ( dom SIFo) holds (SIFo . x) c= (Uo . x)

        proof

          let x be object;

          assume

           A8: x in ( dom SIFo);

          then (ao . x) in ( rng ao) by A5, FUNCT_1:def 3;

          then

          reconsider k = (ao . x) as Element of S by A4;

          set f = (F . k);

          

           A9: ( dom f) = (the Sorts of U1 . k) by FUNCT_2:def 1;

          

           A10: ( rng f) c= (the Sorts of U2 . k) by RELAT_1:def 19;

          SIF = (F .:.: the Sorts of U1) by A2, Def12;

          

          then (SIFo . x) = ((F .:.: the Sorts of U1) . k) by A8, FUNCT_1: 12

          .= (f .: (the Sorts of U1 . k)) by PBOOLE:def 20

          .= ( rng f) by A9, RELAT_1: 113;

          hence thesis by A6, A8, A10, FUNCT_1: 12;

        end;

        

         A11: ( dom x) = ( dom ( the_arity_of o)) by Th6;

         A12:

        now

          let a be object;

          assume

           A13: a in ( dom ( the_arity_of o));

          then

          reconsider n = a as Nat;

          ((G # x) . n) = ((G . (( the_arity_of o) /. n)) . (x . n)) by A11, A13, Def6;

          hence ((G # x) . a) = ((G1 # x) . a) by A11, A13, Def6;

        end;

        ( dom (G # x)) = ( dom ( the_arity_of o)) & ( dom (G1 # x)) = ( dom ( the_arity_of o)) by Th6;

        then (G # x) = (G1 # x) by A12, FUNCT_1: 2;

        then

         A14: ((G . ( the_result_sort_of o)) . (( Den (o,U1)) . x)) = (( Den (o,U2)) . (G # x)) by A1, A2;

        SIF is opers_closed by MSUALG_2:def 9;

        then

         A15: SIF is_closed_on o;

        ( Args (o,IF)) = ( product SIFo) & ( Args (o,U2)) = ( product Uo) by PRALG_2: 3;

        then ( Args (o,IF)) c= ( Args (o,U2)) by A6, A7, CARD_3: 27;

        then (G # x) in ( dom ( Den (o,U2))) by A3;

        then

         A16: (((SIF # ) * the Arity of S) . o) = ( Args (o,IF)) & (G # x) in (( dom ( Den (o,U2))) /\ ( Args (o,IF))) by MSUALG_1:def 4, XBOOLE_0:def 4;

        the Charact of IF = ( Opers (U2,SIF)) by MSUALG_2:def 9;

        

        then ( Den (o,IF)) = (( Opers (U2,SIF)) . o) by MSUALG_1:def 6

        .= (o /. SIF) by MSUALG_2:def 8

        .= (( Den (o,U2)) | (((SIF # ) * the Arity of S) . o)) by A15, MSUALG_2:def 7;

        hence thesis by A14, A16, FUNCT_1: 48;

      end;

      then

       A17: G is_homomorphism (U1,( Image F));

      for i be set st i in the carrier of S holds ( rng (G . i)) = (the Sorts of ( Image F) . i)

      proof

        let i be set;

        assume i in the carrier of S;

        then

        reconsider i as Element of S;

        set g = (G . i);

        the Sorts of ( Image F) = (G .:.: the Sorts of U1) by A1, A2, Def12;

        then

         A18: (the Sorts of ( Image F) . i) = (g .: (the Sorts of U1 . i)) by PBOOLE:def 20;

        ( dom g) = (the Sorts of U1 . i) by FUNCT_2:def 1;

        hence thesis by A18, RELAT_1: 113;

      end;

      then G is "onto";

      hence thesis by A17;

    end;

    theorem :: MSUALG_3:21

    for U1,U2 be non-empty MSAlgebra over S holds for F be ManySortedFunction of U1, U2 st F is_homomorphism (U1,U2) holds ex G be ManySortedFunction of U1, ( Image F) st F = G & G is_epimorphism (U1,( Image F))

    proof

      let U1,U2 be non-empty MSAlgebra over S;

      let F be ManySortedFunction of U1, U2;

      assume

       A1: F is_homomorphism (U1,U2);

      then

      reconsider G = F as ManySortedFunction of U1, ( Image F) by Lm3;

      take G;

      thus thesis by A1, Th20;

    end;

    

     Lm4: for U1,U2 be non-empty MSAlgebra over S holds for U3 be non-empty MSSubAlgebra of U2, F be ManySortedFunction of U1, U2, G be ManySortedFunction of U1, U3 st F = G & G is_homomorphism (U1,U3) holds F is_homomorphism (U1,U2)

    proof

      let U1,U2 be non-empty MSAlgebra over S;

      let U3 be non-empty MSSubAlgebra of U2, F be ManySortedFunction of U1, U2, G be ManySortedFunction of U1, U3;

      assume that

       A1: F = G and

       A2: G is_homomorphism (U1,U3);

      for o be OperSymbol of S st ( Args (o,U1)) <> {} holds for x be Element of ( Args (o,U1)) holds ((F . ( the_result_sort_of o)) . (( Den (o,U1)) . x)) = (( Den (o,U2)) . (F # x))

      proof

        reconsider S3 = the Sorts of U3 as non-empty MSSubset of U2 by MSUALG_2:def 9;

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

        let x be Element of ( Args (o,U1));

        for i be object st i in the carrier of S holds (G . i) is Function of (the Sorts of U1 . i), (the Sorts of U2 . i)

        proof

          reconsider S3 = the Sorts of U3 as non-empty MSSubset of U2 by MSUALG_2:def 9;

          let i be object;

          assume

           A3: i in the carrier of S;

          then

          reconsider g = (G . i) as Function of (the Sorts of U1 . i), (the Sorts of U3 . i) by PBOOLE:def 15;

          the Sorts of U3 is MSSubset of U2 by MSUALG_2:def 9;

          then the Sorts of U3 c= the Sorts of U2 by PBOOLE:def 18;

          then (S3 . i) c= (the Sorts of U2 . i) by A3, PBOOLE:def 2;

          then g is Function of (the Sorts of U1 . i), (the Sorts of U2 . i) by A3, FUNCT_2: 7;

          hence thesis;

        end;

        then

        reconsider G1 = G as ManySortedFunction of U1, U2 by PBOOLE:def 15;

        S3 is opers_closed by MSUALG_2:def 9;

        then

         A4: S3 is_closed_on o;

        the Charact of U3 = ( Opers (U2,S3)) by MSUALG_2:def 9;

        

        then

         A5: ( Den (o,U3)) = (( Opers (U2,S3)) . o) by MSUALG_1:def 6

        .= (o /. S3) by MSUALG_2:def 8

        .= (( Den (o,U2)) | (((S3 # ) * the Arity of S) . o)) by A4, MSUALG_2:def 7;

        

         A6: ( dom x) = ( dom ( the_arity_of o)) by Th6;

         A7:

        now

          let a be object;

          assume

           A8: a in ( dom ( the_arity_of o));

          then

          reconsider n = a as Nat;

          ((G # x) . n) = ((G . (( the_arity_of o) /. n)) . (x . n)) by A6, A8, Def6;

          hence ((G # x) . a) = ((G1 # x) . a) by A6, A8, Def6;

        end;

        ( dom (G # x)) = ( dom ( the_arity_of o)) & ( dom (G1 # x)) = ( dom ( the_arity_of o)) by Th6;

        then

         A9: (G # x) = (G1 # x) by A7, FUNCT_1: 2;

        ( dom ( Den (o,U2))) = ( Args (o,U2)) by FUNCT_2:def 1;

        then

         A10: (((S3 # ) * the Arity of S) . o) = ( Args (o,U3)) & (F # x) in (( dom ( Den (o,U2))) /\ ( Args (o,U3))) by A1, A9, MSUALG_1:def 4, XBOOLE_0:def 4;

        ((F . ( the_result_sort_of o)) . (( Den (o,U1)) . x)) = (( Den (o,U3)) . (F # x)) by A1, A2, A9;

        hence thesis by A5, A10, FUNCT_1: 48;

      end;

      hence thesis;

    end;

    theorem :: MSUALG_3:22

    

     Th22: for U1 be non-empty MSAlgebra over S holds for U2 be non-empty MSSubAlgebra of U1, G be ManySortedFunction of U2, U1 st G = ( id the Sorts of U2) holds G is_monomorphism (U2,U1)

    proof

      let U1 be non-empty MSAlgebra over S;

      let U2 be non-empty MSSubAlgebra of U1, G be ManySortedFunction of U2, U1;

      set F = ( id the Sorts of U2);

      assume

       A1: G = ( id the Sorts of U2);

      for i be set st i in the carrier of S holds (G . i) is one-to-one

      proof

        let i be set;

        assume

         A2: i in the carrier of S;

        then

        reconsider f = (F . i) as Function of (the Sorts of U2 . i), (the Sorts of U2 . i) by PBOOLE:def 15;

        f = ( id (the Sorts of U2 . i)) by A2, Def1;

        hence thesis by A1;

      end;

      then

       A3: G is "1-1" by Th1;

      G is_homomorphism (U2,U1) by A1, Lm4, Th9;

      hence thesis by A3;

    end;

    theorem :: MSUALG_3:23

    for U1,U2 be non-empty MSAlgebra over S holds for F be ManySortedFunction of U1, U2 st F is_homomorphism (U1,U2) holds ex F1 be ManySortedFunction of U1, ( Image F), F2 be ManySortedFunction of ( Image F), U2 st F1 is_epimorphism (U1,( Image F)) & F2 is_monomorphism (( Image F),U2) & F = (F2 ** F1)

    proof

      let U1,U2 be non-empty MSAlgebra over S;

      let F be ManySortedFunction of U1, U2;

      assume

       A1: F is_homomorphism (U1,U2);

      then

      reconsider F1 = F as ManySortedFunction of U1, ( Image F) by Lm3;

      for H be ManySortedFunction of ( Image F), ( Image F) holds H is ManySortedFunction of ( Image F), U2

      proof

        let H be ManySortedFunction of ( Image F), ( Image F);

        for i be object st i in the carrier of S holds (H . i) is Function of (the Sorts of ( Image F) . i), (the Sorts of U2 . i)

        proof

          let i be object;

          assume

           A2: i in the carrier of S;

          then

          reconsider f = (F . i) as Function of (the Sorts of U1 . i), (the Sorts of U2 . i) by PBOOLE:def 15;

          

           A3: ( dom f) = (the Sorts of U1 . i) by A2, FUNCT_2:def 1;

          reconsider h = (H . i) as Function of (the Sorts of ( Image F) . i), (the Sorts of ( Image F) . i) by A2, PBOOLE:def 15;

          

           A4: ( rng f) c= (the Sorts of U2 . i) by RELAT_1:def 19;

          the Sorts of ( Image F) = (F .:.: the Sorts of U1) by A1, Def12;

          

          then (the Sorts of ( Image F) . i) = (f .: (the Sorts of U1 . i)) by A2, PBOOLE:def 20

          .= ( rng f) by A3, RELAT_1: 113;

          then h is Function of (the Sorts of ( Image F) . i), (the Sorts of U2 . i) by A4, FUNCT_2: 7;

          hence thesis;

        end;

        hence thesis by PBOOLE:def 15;

      end;

      then

      reconsider F2 = ( id the Sorts of ( Image F)) as ManySortedFunction of ( Image F), U2;

      take F1, F2;

      thus F1 is_epimorphism (U1,( Image F)) by A1, Th20;

      thus F2 is_monomorphism (( Image F),U2) by Th22;

      thus thesis by Th4;

    end;

    theorem :: MSUALG_3:24

    for S holds for U1,U2 be MSAlgebra over S holds for o holds for F be ManySortedFunction of U1, U2 holds for x be Element of ( Args (o,U1)), f,u be Function st x = f & x in ( Args (o,U1)) & u in ( Args (o,U2)) holds u = (F # x) iff for n st n in ( dom f) holds (u . n) = ((F . (( the_arity_of o) /. n)) . (f . n)) by Lm1;