msualg_9.miz



    begin

    reserve a,I for set,

S for non empty non void ManySortedSign;

    registration

      let I be set, M be ManySortedSet of I;

      cluster finite-yielding for Element of ( Bool M);

      existence

      proof

        ( EmptyMS I) c= M by PBOOLE: 43;

        then ( EmptyMS I) is ManySortedSubset of M by PBOOLE:def 18;

        then

        reconsider A = ( EmptyMS I) as Element of ( Bool M) by CLOSURE2:def 1;

        take A;

        thus thesis;

      end;

    end

    registration

      let I be set, M be non-empty ManySortedSet of I;

      cluster non-empty finite-yielding for ManySortedSubset of M;

      existence

      proof

        defpred P[ object, object] means ex a be Element of (M . $1) st $2 = {a};

         A1:

        now

          let i be object such that i in I;

          set a = the Element of (M . i);

          reconsider j = {a} as object;

          take j;

          thus P[i, j];

        end;

        consider C be ManySortedSet of I such that

         A2: for i be object st i in I holds P[i, (C . i)] from PBOOLE:sch 3( A1);

        C is ManySortedSubset of M

        proof

          let i be object;

          assume

           A3: i in I;

          then

           A4: (M . i) is non empty;

          let q be object;

          consider a be Element of (M . i) such that

           A5: (C . i) = {a} by A2, A3;

          assume q in (C . i);

          then q = a by A5, TARSKI:def 1;

          hence thesis by A4;

        end;

        then

        reconsider C as ManySortedSubset of M;

        take C;

        thus C is non-empty

        proof

          let i be object;

          assume i in I;

          then ex a be Element of (M . i) st (C . i) = {a} by A2;

          hence thesis;

        end;

        let i be object;

        assume i in I;

        then ex a be Element of (M . i) st (C . i) = {a} by A2;

        hence thesis;

      end;

    end

    registration

      let S be non empty non void ManySortedSign, A be non-empty MSAlgebra over S, o be OperSymbol of S;

      cluster -> FinSequence-like for Element of ( Args (o,A));

      coherence

      proof

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

        ( dom x) = ( dom ( the_arity_of o)) by MSUALG_6: 2;

        then

        consider n be Nat such that

         A1: ( dom x) = ( Seg n) by FINSEQ_1:def 2;

        take n;

        thus thesis by A1;

      end;

    end

    registration

      let S be non void non empty ManySortedSign, I be set, s be SortSymbol of S, F be MSAlgebra-Family of I, S;

      cluster -> Function-like Relation-like for Element of (( SORTS F) . s);

      coherence

      proof

        let x be Element of (( SORTS F) . s);

        x is Element of ( product ( Carrier (F,s))) by PRALG_2:def 10;

        hence thesis;

      end;

    end

    registration

      let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S;

      cluster ( FreeGen X) -> free non-empty;

      coherence by MSAFREE: 14, MSAFREE: 16;

    end

    registration

      let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S;

      cluster ( FreeMSA X) -> free;

      coherence by MSAFREE: 17;

    end

    registration

      let S be non empty non void ManySortedSign, A,B be non-empty MSAlgebra over S;

      cluster [:A, B:] -> non-empty;

      coherence

      proof

         [:A, B:] = MSAlgebra (# [|the Sorts of A, the Sorts of B|], [[:the Charact of A, the Charact of B:]] #) by PRALG_2:def 8;

        hence the Sorts of [:A, B:] is non-empty;

      end;

    end

    theorem :: MSUALG_9:1

    for X,Y be set, f be Function st a in ( dom f) & (f . a) in [:X, Y:] holds (f . a) = [(( pr1 f) . a), (( pr2 f) . a)]

    proof

      let X,Y be set, f be Function such that

       A1: a in ( dom f) and

       A2: (f . a) in [:X, Y:];

      (( pr1 f) . a) = ((f . a) `1 ) & (( pr2 f) . a) = ((f . a) `2 ) by A1, MCART_1:def 12, MCART_1:def 13;

      hence thesis by A2, MCART_1: 21;

    end;

    theorem :: MSUALG_9:2

    

     Th2: for X be non empty set, Y be set, f be Function of X, {Y} holds ( rng f) = {Y}

    proof

      let X be non empty set, Y be set, f be Function of X, {Y};

      thus ( rng f) c= {Y};

      let q be object;

      consider x be object such that

       A1: x in X by XBOOLE_0:def 1;

      assume q in {Y};

      then

       A2: ( dom f) = X & q = Y by FUNCT_2:def 1, TARSKI:def 1;

      (f . x) = Y by A1, FUNCT_2: 50;

      hence thesis by A2, A1, FUNCT_1:def 3;

    end;

    theorem :: MSUALG_9:3

    

     Th3: ( Class ( nabla I)) c= {I}

    proof

      let q be object;

      assume q in ( Class ( nabla I));

      then

      consider x be object such that

       A1: x in I and

       A2: q = ( Class (( nabla I),x)) by EQREL_1:def 3;

      ( Class (( nabla I),x)) = I by A1, EQREL_1: 26;

      hence thesis by A2, TARSKI:def 1;

    end;

    theorem :: MSUALG_9:4

    

     Th4: for I be non empty set holds ( Class ( nabla I)) = {I}

    proof

      let I be non empty set;

      consider a be object such that

       A1: a in I by XBOOLE_0:def 1;

      thus ( Class ( nabla I)) c= {I} by Th3;

      let q be object;

      assume q in {I};

      then

       A2: q = I by TARSKI:def 1;

      ( Class (( nabla I),a)) = I by A1, EQREL_1: 26;

      hence thesis by A2, A1, EQREL_1:def 3;

    end;

    theorem :: MSUALG_9:5

    

     Th5: ex A be ManySortedSet of I st {A} = (I --> {a})

    proof

      reconsider A = (I --> a) as ManySortedSet of I;

      take A;

      now

        let i be object;

        assume

         A1: i in I;

        

        hence ( {A} . i) = {(A . i)} by PZFMISC1:def 1

        .= {a} by A1, FUNCOP_1: 7

        .= ((I --> {a}) . i) by A1, FUNCOP_1: 7;

      end;

      hence thesis;

    end;

    theorem :: MSUALG_9:6

    for A be ManySortedSet of I holds ex B be non-empty ManySortedSet of I st A c= B

    proof

      let A be ManySortedSet of I;

      deffunc F( object) = ( { {} } \/ (A . $1));

      consider f be ManySortedSet of I such that

       A1: for i be object st i in I holds (f . i) = F(i) from PBOOLE:sch 4;

      f is non-empty

      proof

        let i be object;

        assume i in I;

        then (f . i) = ( { {} } \/ (A . i)) by A1;

        hence thesis;

      end;

      then

      reconsider f as non-empty ManySortedSet of I;

      take f;

      let i be object;

      assume i in I;

      then (f . i) = ((A . i) \/ { {} }) by A1;

      hence thesis by XBOOLE_1: 7;

    end;

    theorem :: MSUALG_9:7

    for M be non-empty ManySortedSet of I holds for B be finite-yielding ManySortedSubset of M holds ex C be non-empty finite-yielding ManySortedSubset of M st B c= C

    proof

      let M be non-empty ManySortedSet of I, B be finite-yielding ManySortedSubset of M;

      defpred P[ object, object] means ex a be Element of (M . $1) st $2 = ( {a} \/ (B . $1));

       A1:

      now

        let i be object such that i in I;

        set a = the Element of (M . i);

        reconsider j = ( {a} \/ (B . i)) as object;

        take j;

        thus P[i, j];

      end;

      consider C be ManySortedSet of I such that

       A2: for i be object st i in I holds P[i, (C . i)] from PBOOLE:sch 3( A1);

      

       A3: C is ManySortedSubset of M

      proof

        let i be object;

        assume

         A4: i in I;

        then

        consider a be Element of (M . i) such that

         A5: (C . i) = ( {a} \/ (B . i)) by A2;

        let q be object;

        assume q in (C . i);

        then

         A6: q in {a} or q in (B . i) by A5, XBOOLE_0:def 3;

        B c= M by PBOOLE:def 18;

        then (B . i) c= (M . i) by A4;

        then

         A7: q = a or q in (M . i) by A6, TARSKI:def 1;

        (M . i) is non empty by A4;

        hence thesis by A7;

      end;

      

       A8: C is finite-yielding

      proof

        let i be object;

        assume

         A9: i in I;

        reconsider b = (B . i) as finite set;

        consider a be Element of (M . i) such that

         A10: (C . i) = ( {a} \/ (B . i)) by A2, A9;

        thus thesis by A10;

      end;

      C is non-empty

      proof

        let i be object;

        assume i in I;

        then ex a be Element of (M . i) st (C . i) = ( {a} \/ (B . i)) by A2;

        hence thesis;

      end;

      then

      reconsider C as non-empty finite-yielding ManySortedSubset of M by A3, A8;

      take C;

      let i be object;

      assume i in I;

      then ex a be Element of (M . i) st (C . i) = ( {a} \/ (B . i)) by A2;

      hence thesis by XBOOLE_1: 7;

    end;

    theorem :: MSUALG_9:8

    for A,B be ManySortedSet of I holds for F,G be ManySortedFunction of A, {B} holds F = G

    proof

      let A,B be ManySortedSet of I, F,G be ManySortedFunction of A, {B};

      now

        let i be object;

        assume

         A1: i in I;

        then

         A2: ( {B} . i) = {(B . i)} by PZFMISC1:def 1;

        (F . i) is Function of (A . i), ( {B} . i) & (G . i) is Function of (A . i), ( {B} . i) by A1, PBOOLE:def 15;

        hence (F . i) = (G . i) by A2, FUNCT_2: 51;

      end;

      hence thesis;

    end;

    theorem :: MSUALG_9:9

    

     Th9: for A be non-empty ManySortedSet of I, B be ManySortedSet of I holds for F be ManySortedFunction of A, {B} holds F is "onto"

    proof

      let A be non-empty ManySortedSet of I, B be ManySortedSet of I, F be ManySortedFunction of A, {B};

      let i be set;

      assume

       A1: i in I;

      then ( {B} . i) = {(B . i)} & (F . i) is Function of (A . i), ( {B} . i) by PBOOLE:def 15, PZFMISC1:def 1;

      hence thesis by A1, Th2;

    end;

    theorem :: MSUALG_9:10

    

     Th10: for A be ManySortedSet of I, B be non-empty ManySortedSet of I holds for F be ManySortedFunction of {A}, B holds F is "1-1"

    proof

      let A be ManySortedSet of I, B be non-empty ManySortedSet of I, F be ManySortedFunction of {A}, B;

      now

        let i be set;

        assume i in I;

        then ( {A} . i) = {(A . i)} & (F . i) is Function of ( {A} . i), (B . i) by PBOOLE:def 15, PZFMISC1:def 1;

        hence (F . i) is one-to-one by PARTFUN1: 17;

      end;

      hence thesis by MSUALG_3: 1;

    end;

    theorem :: MSUALG_9:11

    for X be non-empty ManySortedSet of the carrier of S holds ( Reverse X) is "1-1"

    proof

      let X be non-empty ManySortedSet of the carrier of S;

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

      proof

        set D = ( DTConMSA X);

        let i be set;

        assume i in the carrier of S;

        then

        reconsider s = i as SortSymbol of S;

        set f = (( Reverse X) . s);

        let x1,x2 be object such that

         A1: x1 in ( dom (( Reverse X) . i)) and

         A2: x2 in ( dom (( Reverse X) . i)) and

         A3: ((( Reverse X) . i) . x1) = ((( Reverse X) . i) . x2);

        

         A4: f = ( Reverse (s,X)) by MSAFREE:def 18;

        then

         A5: ( dom f) = ( FreeGen (s,X)) by FUNCT_2:def 1;

        then

        consider a2 be set such that

         A6: a2 in (X . s) and

         A7: x2 = ( root-tree [a2, s]) by A2, MSAFREE:def 15;

        

         A8: [a2, s] in ( Terminals D) by A6, MSAFREE: 7;

        then

        reconsider t2 = [a2, s] as Symbol of D;

        (t2 `2 ) = s;

        then ( root-tree t2) in { ( root-tree tt) where tt be Symbol of D : tt in ( Terminals D) & (tt `2 ) = s } by A8;

        then ( root-tree t2) in ( FreeGen (s,X)) by MSAFREE: 13;

        

        then

         A9: (f . x2) = ( [a2, s] `1 ) by A4, A7, MSAFREE:def 17

        .= a2;

        consider a1 be set such that

         A10: a1 in (X . s) and

         A11: x1 = ( root-tree [a1, s]) by A1, A5, MSAFREE:def 15;

        

         A12: [a1, s] in ( Terminals D) by A10, MSAFREE: 7;

        then

        reconsider t1 = [a1, s] as Symbol of D;

        (t1 `2 ) = s;

        then ( root-tree t1) in { ( root-tree tt) where tt be Symbol of D : tt in ( Terminals D) & (tt `2 ) = s } by A12;

        then ( root-tree t1) in ( FreeGen (s,X)) by MSAFREE: 13;

        

        then (f . x1) = ( [a1, s] `1 ) by A4, A11, MSAFREE:def 17

        .= a1;

        hence thesis by A3, A11, A7, A9;

      end;

      hence thesis by MSUALG_3: 1;

    end;

    theorem :: MSUALG_9:12

    for A be non-empty finite-yielding ManySortedSet of I holds ex F be ManySortedFunction of (I --> NAT ), A st F is "onto"

    proof

      let A be non-empty finite-yielding ManySortedSet of I;

      defpred P[ object, object] means ex f be sequence of (A . $1) st $2 = f & ( rng f) = (A . $1);

      

       A1: for i be object st i in I holds ex j be object st P[i, j]

      proof

        let i be object;

        assume

         A2: i in I;

        consider f be sequence of (A . i) such that

         A3: ( rng f) = (A . i) by A2, CARD_3: 96;

        take f;

        thus thesis by A3;

      end;

      consider F be ManySortedSet of I such that

       A4: for i be object st i in I holds P[i, (F . i)] from PBOOLE:sch 3( A1);

      F is ManySortedFunction of (I --> NAT ), A

      proof

        let i be object;

        assume i in I;

        then (ex f be sequence of (A . i) st (F . i) = f & ( rng f) = (A . i)) & ((I --> NAT ) . i) = NAT by A4, FUNCOP_1: 7;

        hence thesis;

      end;

      then

      reconsider F as ManySortedFunction of (I --> NAT ), A;

      take F;

      let i be set;

      assume i in I;

      then ex f be sequence of (A . i) st (F . i) = f & ( rng f) = (A . i) by A4;

      hence thesis;

    end;

    theorem :: MSUALG_9:13

    for S be non empty ManySortedSign holds for A be non-empty MSAlgebra over S holds for f,g be Element of ( product the Sorts of A) st for i be object holds (( proj (the Sorts of A,i)) . f) = (( proj (the Sorts of A,i)) . g) holds f = g

    proof

      let S be non empty ManySortedSign, A be non-empty MSAlgebra over S, f,g be Element of ( product the Sorts of A) such that

       A1: for i be object holds (( proj (the Sorts of A,i)) . f) = (( proj (the Sorts of A,i)) . g);

      set X = the Sorts of A;

      now

        

        thus ( dom f) = ( dom X) by CARD_3: 9

        .= ( dom g) by CARD_3: 9;

        let x be object such that x in ( dom f);

        

         A2: ( dom ( proj (X,x))) = ( product X) by CARD_3:def 16;

        

        hence (f . x) = (( proj (X,x)) . f) by CARD_3:def 16

        .= (( proj (X,x)) . g) by A1

        .= (g . x) by A2, CARD_3:def 16;

      end;

      hence thesis;

    end;

    theorem :: MSUALG_9:14

    for I be non empty set holds for s be Element of S holds for A be MSAlgebra-Family of I, S holds for f,g be Element of ( product ( Carrier (A,s))) st for a be Element of I holds (( proj (( Carrier (A,s)),a)) . f) = (( proj (( Carrier (A,s)),a)) . g) holds f = g

    proof

      let I be non empty set, s be Element of S, A be MSAlgebra-Family of I, S, f,g be Element of ( product ( Carrier (A,s))) such that

       A1: for a be Element of I holds (( proj (( Carrier (A,s)),a)) . f) = (( proj (( Carrier (A,s)),a)) . g);

      now

        ( dom f) = ( dom ( Carrier (A,s))) by CARD_3: 9;

        hence ( dom f) = ( dom g) by CARD_3: 9;

        let x be object such that

         A2: x in ( dom f);

        

         A3: ( dom ( proj (( Carrier (A,s)),x))) = ( product ( Carrier (A,s))) by CARD_3:def 16;

        

        hence (f . x) = (( proj (( Carrier (A,s)),x)) . f) by CARD_3:def 16

        .= (( proj (( Carrier (A,s)),x)) . g) by A1, A2

        .= (g . x) by A3, CARD_3:def 16;

      end;

      hence thesis;

    end;

    theorem :: MSUALG_9:15

    for A,B be non-empty MSAlgebra over S holds for C be non-empty MSSubAlgebra of A holds for h1 be ManySortedFunction of B, C st h1 is_homomorphism (B,C) holds for h2 be ManySortedFunction of B, A st h1 = h2 holds h2 is_homomorphism (B,A)

    proof

      let A,B be non-empty MSAlgebra over S, C be non-empty MSSubAlgebra of A, h1 be ManySortedFunction of B, C such that

       A1: h1 is_homomorphism (B,C);

      the Sorts of C is ManySortedSubset of the Sorts of A by MSUALG_2:def 9;

      then ( id the Sorts of C) is ManySortedFunction of C, A by EXTENS_1: 5;

      then

      consider G be ManySortedFunction of C, A such that

       A2: G = ( id the Sorts of C);

      G is_monomorphism (C,A) by A2, MSUALG_3: 22;

      then

       A3: G is_homomorphism (C,A);

      

       A4: (G ** h1) = h1 by A2, MSUALG_3: 4;

      let h2 be ManySortedFunction of B, A;

      assume h1 = h2;

      hence thesis by A1, A4, A3, MSUALG_3: 10;

    end;

    theorem :: MSUALG_9:16

    for A,B be non-empty MSAlgebra over S holds for F be ManySortedFunction of A, B st F is_monomorphism (A,B) holds (A,( Image F)) are_isomorphic

    proof

      let A,B be non-empty MSAlgebra over S, F be ManySortedFunction of A, B;

      assume

       A1: F is_monomorphism (A,B);

      then F is_homomorphism (A,B);

      then

      consider G be ManySortedFunction of A, ( Image F) such that

       A2: G = F and

       A3: G is_epimorphism (A,( Image F)) by MSUALG_3: 21;

      take G;

      thus G is_epimorphism (A,( Image F)) by A3;

      thus G is_homomorphism (A,( Image F)) by A3;

      thus thesis by A1, A2;

    end;

    theorem :: MSUALG_9:17

    

     Th17: for A,B be non-empty MSAlgebra over S holds for F be ManySortedFunction of A, B st F is "onto" holds for o be OperSymbol of S holds for x be Element of ( Args (o,B)) holds ex y be Element of ( Args (o,A)) st (F # y) = x

    proof

      let A,B be non-empty MSAlgebra over S, F be ManySortedFunction of A, B such that

       A1: F is "onto";

      let o be OperSymbol of S, t be Element of ( Args (o,B));

      set D = ( len ( the_arity_of o));

      defpred P[ object, object] means ex y1 be Element of (the Sorts of A . (( the_arity_of o) /. $1)) st ((F . (( the_arity_of o) /. $1)) . y1) = (t . $1) & $2 = y1;

      

       A2: for k be Element of NAT st k in ( Seg D) holds ex x be object st P[k, x]

      proof

        let k be Element of NAT ;

        assume k in ( Seg D);

        then

         A3: k in ( dom ( the_arity_of o)) by FINSEQ_1:def 3;

        set s = (( the_arity_of o) /. k);

        

         A4: (t . k) in (the Sorts of B . s) by A3, MSUALG_6: 2;

        ( rng (F . s)) = (the Sorts of B . s) by A1;

        then

        consider y1 be object such that

         A5: y1 in (the Sorts of A . s) and

         A6: ((F . s) . y1) = (t . k) by A4, FUNCT_2: 11;

        reconsider y2 = y1 as Element of (the Sorts of A . s) by A5;

        take y1;

        take y2;

        thus thesis by A6;

      end;

      consider p be FinSequence such that

       A7: ( dom p) = ( Seg D) and

       A8: for k be Element of NAT st k in ( Seg D) holds P[k, (p . k)] from MSUALG_8:sch 1( A2);

      

       A9: ( len p) = ( len ( the_arity_of o)) by A7, FINSEQ_1:def 3;

      for k be Nat st k in ( dom p) holds (p . k) in (the Sorts of A . (( the_arity_of o) /. k))

      proof

        let k be Nat;

        assume k in ( dom p);

        then ex y1 be Element of (the Sorts of A . (( the_arity_of o) /. k)) st ((F . (( the_arity_of o) /. k)) . y1) = (t . k) & (p . k) = y1 by A7, A8;

        hence thesis;

      end;

      then

      reconsider p as Element of ( Args (o,A)) by A9, MSAFREE2: 5;

      set fp = (F # p);

      take p;

      reconsider E = (the Sorts of B * ( the_arity_of o)) as non-empty ManySortedSet of ( dom ( the_arity_of o));

      

       A10: ( Args (o,B)) = ( product E) by PRALG_2: 3;

      

       A11: ( Seg D) = ( dom ( the_arity_of o)) by FINSEQ_1:def 3

      .= ( dom (the Sorts of B * ( the_arity_of o))) by PRALG_2: 3

      .= ( dom t) by A10, CARD_3: 9;

      

       A12: for k be Nat st k in ( dom t) holds (fp . k) = (t . k)

      proof

        let k be Nat;

        assume

         A13: k in ( dom t);

        then ex y1 be Element of (the Sorts of A . (( the_arity_of o) /. k)) st ((F . (( the_arity_of o) /. k)) . y1) = (t . k) & (p . k) = y1 by A11, A8;

        hence thesis by A11, A7, A13, MSUALG_3:def 6;

      end;

      ( dom fp) = ( dom (the Sorts of B * ( the_arity_of o))) by A10, CARD_3: 9

      .= ( dom t) by A10, CARD_3: 9;

      hence thesis by A12;

    end;

    theorem :: MSUALG_9:18

    

     Th18: for A be non-empty MSAlgebra over S, o be OperSymbol of S holds for x be Element of ( Args (o,A)) holds (( Den (o,A)) . x) in (the Sorts of A . ( the_result_sort_of o))

    proof

      let A be non-empty MSAlgebra over S, o be OperSymbol of S, x be Element of ( Args (o,A));

      (( Den (o,A)) . x) is Element of (the Sorts of A . (the ResultSort of S . o)) by FUNCT_2: 15;

      hence thesis;

    end;

    theorem :: MSUALG_9:19

    

     Th19: for A,B,C be non-empty MSAlgebra over S holds for F1 be ManySortedFunction of A, B holds for F2 be ManySortedFunction of A, C st F1 is_epimorphism (A,B) & F2 is_homomorphism (A,C) holds for G be ManySortedFunction of B, C st (G ** F1) = F2 holds G is_homomorphism (B,C)

    proof

      let A,B,C be non-empty MSAlgebra over S, F1 be ManySortedFunction of A, B, F2 be ManySortedFunction of A, C such that

       A1: F1 is_epimorphism (A,B) and

       A2: F2 is_homomorphism (A,C);

      let G be ManySortedFunction of B, C such that

       A3: (G ** F1) = F2;

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

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

      F1 is "onto" by A1;

      then

      consider y be Element of ( Args (o,A)) such that

       A4: (F1 # y) = x by Th17;

      set r = ( the_result_sort_of o);

      F1 is_homomorphism (A,B) by A1;

      then

       A5: ((F1 . r) . (( Den (o,A)) . y)) = (( Den (o,B)) . x) by A4;

      

       A6: ((F2 . r) . (( Den (o,A)) . y)) = (((G . r) * (F1 . r)) . (( Den (o,A)) . y)) by A3, MSUALG_3: 2

      .= ((G . r) . (( Den (o,B)) . x)) by A5, Th18, FUNCT_2: 15;

      ((F2 . r) . (( Den (o,A)) . y)) = (( Den (o,C)) . ((G ** F1) # y)) by A2, A3

      .= (( Den (o,C)) . (G # x)) by A4, MSUALG_3: 8;

      hence ((G . ( the_result_sort_of o)) . (( Den (o,B)) . x)) = (( Den (o,C)) . (G # x)) by A6;

    end;

    reserve A,M for ManySortedSet of I,

B,C for non-empty ManySortedSet of I;

    definition

      let I be set;

      let A be ManySortedSet of I;

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

      let F be ManySortedFunction of A, [|B, C|];

      :: MSUALG_9:def1

      func Mpr1 F -> ManySortedFunction of A, B means

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

      existence

      proof

        deffunc G( object) = ( pr1 (F . $1));

        consider X be ManySortedSet of I such that

         A1: for i be object st i in I holds (X . i) = G(i) from PBOOLE:sch 4;

        X is ManySortedFunction of A, B

        proof

          let i be object;

          assume

           A2: i in I;

          then

          reconsider Bi = (B . i) as non empty set;

          

           A3: (X . i) = ( pr1 (F . i)) by A1, A2;

          then

          reconsider Xi = (X . i) as Function;

          

           A4: (F . i) is Function of (A . i), ( [|B, C|] . i) by A2, PBOOLE:def 15;

          

           A5: ( rng Xi) c= Bi

          proof

            let q be object;

            assume q in ( rng Xi);

            then

            consider x be object such that

             A6: x in ( dom Xi) and

             A7: (Xi . x) = q by FUNCT_1:def 3;

            x in ( dom (F . i)) by A3, A6, MCART_1:def 12;

            then

             A8: (Xi . x) = (((F . i) . x) `1 ) & ((F . i) . x) in ( rng (F . i)) by A3, FUNCT_1:def 3, MCART_1:def 12;

            ( rng (F . i)) c= ( [|B, C|] . i) by A4, RELAT_1:def 19;

            then

             A9: ( rng (F . i)) c= [:(B . i), (C . i):] by A2, PBOOLE:def 16;

            assume not q in Bi;

            hence contradiction by A7, A9, A8, MCART_1: 10;

          end;

          ( dom (F . i)) = (A . i) by A2, A4, FUNCT_2:def 1;

          then ( dom Xi) = (A . i) by A3, MCART_1:def 12;

          hence thesis by A5, FUNCT_2:def 1, RELSET_1: 4;

        end;

        then

        reconsider X as ManySortedFunction of A, B;

        take X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let M,N be ManySortedFunction of A, B such that

         A10: for i be set st i in I holds (M . i) = ( pr1 (F . i)) and

         A11: for i be set st i in I holds (N . i) = ( pr1 (F . i));

        now

          let i be object;

          assume

           A12: i in I;

          

          hence (M . i) = ( pr1 (F . i)) by A10

          .= (N . i) by A11, A12;

        end;

        hence M = N;

      end;

      :: MSUALG_9:def2

      func Mpr2 F -> ManySortedFunction of A, C means

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

      existence

      proof

        deffunc G( object) = ( pr2 (F . $1));

        consider X be ManySortedSet of I such that

         A13: for i be object st i in I holds (X . i) = G(i) from PBOOLE:sch 4;

        X is ManySortedFunction of A, C

        proof

          let i be object;

          assume

           A14: i in I;

          then

          reconsider Ci = (C . i) as non empty set;

          

           A15: (X . i) = ( pr2 (F . i)) by A13, A14;

          then

          reconsider Xi = (X . i) as Function;

          

           A16: (F . i) is Function of (A . i), ( [|B, C|] . i) by A14, PBOOLE:def 15;

          

           A17: ( rng Xi) c= Ci

          proof

            let q be object;

            assume q in ( rng Xi);

            then

            consider x be object such that

             A18: x in ( dom Xi) and

             A19: (Xi . x) = q by FUNCT_1:def 3;

            x in ( dom (F . i)) by A15, A18, MCART_1:def 13;

            then

             A20: (Xi . x) = (((F . i) . x) `2 ) & ((F . i) . x) in ( rng (F . i)) by A15, FUNCT_1:def 3, MCART_1:def 13;

            ( rng (F . i)) c= ( [|B, C|] . i) by A16, RELAT_1:def 19;

            then

             A21: ( rng (F . i)) c= [:(B . i), (C . i):] by A14, PBOOLE:def 16;

            assume not q in Ci;

            hence contradiction by A19, A21, A20, MCART_1: 10;

          end;

          ( dom (F . i)) = (A . i) by A14, A16, FUNCT_2:def 1;

          then ( dom Xi) = (A . i) by A15, MCART_1:def 13;

          hence thesis by A17, FUNCT_2:def 1, RELSET_1: 4;

        end;

        then

        reconsider X as ManySortedFunction of A, C;

        take X;

        thus thesis by A13;

      end;

      uniqueness

      proof

        let M,N be ManySortedFunction of A, C such that

         A22: for i be set st i in I holds (M . i) = ( pr2 (F . i)) and

         A23: for i be set st i in I holds (N . i) = ( pr2 (F . i));

        now

          let i be object;

          assume

           A24: i in I;

          

          hence (M . i) = ( pr2 (F . i)) by A22

          .= (N . i) by A23, A24;

        end;

        hence M = N;

      end;

    end

    theorem :: MSUALG_9:20

    for F be ManySortedFunction of A, [|(I --> {a}), (I --> {a})|] holds ( Mpr1 F) = ( Mpr2 F)

    proof

      let F be ManySortedFunction of A, [|(I --> {a}), (I --> {a})|];

      now

        let i be object;

        

         A1: ( dom ( pr2 (F . i))) = ( dom (F . i)) by MCART_1:def 13;

        assume

         A2: i in I;

         A3:

        now

          let y be object such that

           A4: y in ( dom (F . i));

          

           A5: ((F . i) . y) in ( rng (F . i)) by A4, FUNCT_1:def 3;

          (F . i) is Function of (A . i), ( [|(I --> {a}), (I --> {a})|] . i) by A2, PBOOLE:def 15;

          then ( rng (F . i)) c= ( [|(I --> {a}), (I --> {a})|] . i) by RELAT_1:def 19;

          then

           A6: ( rng (F . i)) c= [:((I --> {a}) . i), ((I --> {a}) . i):] by A2, PBOOLE:def 16;

          then (((F . i) . y) `1 ) in ((I --> {a}) . i) by A5, MCART_1: 10;

          then

           A7: (((F . i) . y) `1 ) in {a} by A2, FUNCOP_1: 7;

          (((F . i) . y) `2 ) in ((I --> {a}) . i) by A5, A6, MCART_1: 10;

          then

           A8: (((F . i) . y) `2 ) in {a} by A2, FUNCOP_1: 7;

          

          thus (( pr2 (F . i)) . y) = (((F . i) . y) `2 ) by A4, MCART_1:def 13

          .= a by A8, TARSKI:def 1

          .= (((F . i) . y) `1 ) by A7, TARSKI:def 1;

        end;

        (( Mpr1 F) . i) = ( pr1 (F . i)) & (( Mpr2 F) . i) = ( pr2 (F . i)) by A2, Def1, Def2;

        hence (( Mpr1 F) . i) = (( Mpr2 F) . i) by A1, A3, MCART_1:def 12;

      end;

      hence thesis;

    end;

    theorem :: MSUALG_9:21

    for F be ManySortedFunction of A, [|B, C|] st F is "onto" holds ( Mpr1 F) is "onto"

    proof

      let F be ManySortedFunction of A, [|B, C|] such that

       A1: F is "onto";

      let i be set;

      assume

       A2: i in I;

      then

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

      ( rng m) = (B . i)

      proof

        thus ( rng m) c= (B . i);

        let a be object such that

         A3: a in (B . i);

        consider z be object such that

         A4: z in ( [|B, C|] . i) by A2, XBOOLE_0:def 1;

        set p = [a, (z `2 )];

        z in [:(B . i), (C . i):] by A2, A4, PBOOLE:def 16;

        then

         A5: (p `2 ) in (C . i) by MCART_1: 10;

        (p `1 ) in (B . i) by A3;

        then p in [:(B . i), (C . i):] by A5, ZFMISC_1:def 2;

        then

         A6: p in ( [|B, C|] . i) by A2, PBOOLE:def 16;

        

         A7: ( dom m) = (A . i) by A2, FUNCT_2:def 1;

        

         A8: (F . i) is Function of (A . i), ( [|B, C|] . i) by A2, PBOOLE:def 15;

        then

         A9: ( dom (F . i)) = (A . i) by A2, FUNCT_2:def 1;

        ( rng (F . i)) = ( [|B, C|] . i) by A1, A2;

        then

        consider b be object such that

         A10: b in (A . i) and

         A11: ((F . i) . b) = p by A8, A6, FUNCT_2: 11;

        (m . b) = (( pr1 (F . i)) . b) by A2, Def1

        .= (p `1 ) by A10, A11, A9, MCART_1:def 12

        .= a;

        hence thesis by A10, A7, FUNCT_1:def 3;

      end;

      hence thesis;

    end;

    theorem :: MSUALG_9:22

    for F be ManySortedFunction of A, [|B, C|] st F is "onto" holds ( Mpr2 F) is "onto"

    proof

      let F be ManySortedFunction of A, [|B, C|] such that

       A1: F is "onto";

      let i be set;

      assume

       A2: i in I;

      then

      reconsider m = (( Mpr2 F) . i) as Function of (A . i), (C . i) by PBOOLE:def 15;

      ( rng m) = (C . i)

      proof

        thus ( rng m) c= (C . i);

        let a be object such that

         A3: a in (C . i);

        consider z be object such that

         A4: z in ( [|B, C|] . i) by A2, XBOOLE_0:def 1;

        set p = [(z `1 ), a];

        z in [:(B . i), (C . i):] by A2, A4, PBOOLE:def 16;

        then

         A5: (p `1 ) in (B . i) by MCART_1: 10;

        (p `2 ) in (C . i) by A3;

        then p in [:(B . i), (C . i):] by A5, ZFMISC_1:def 2;

        then

         A6: p in ( [|B, C|] . i) by A2, PBOOLE:def 16;

        

         A7: ( dom m) = (A . i) by A2, FUNCT_2:def 1;

        

         A8: (F . i) is Function of (A . i), ( [|B, C|] . i) by A2, PBOOLE:def 15;

        then

         A9: ( dom (F . i)) = (A . i) by A2, FUNCT_2:def 1;

        ( rng (F . i)) = ( [|B, C|] . i) by A1, A2;

        then

        consider b be object such that

         A10: b in (A . i) and

         A11: ((F . i) . b) = p by A8, A6, FUNCT_2: 11;

        (m . b) = (( pr2 (F . i)) . b) by A2, Def2

        .= (p `2 ) by A10, A11, A9, MCART_1:def 13

        .= a;

        hence thesis by A10, A7, FUNCT_1:def 3;

      end;

      hence thesis;

    end;

    theorem :: MSUALG_9:23

    for F be ManySortedFunction of A, [|B, C|] st M in ( doms F) holds for i be set st i in I holds ((F .. M) . i) = [((( Mpr1 F) .. M) . i), ((( Mpr2 F) .. M) . i)]

    proof

      let F be ManySortedFunction of A, [|B, C|] such that

       A1: M in ( doms F);

      let i be set;

      assume

       A2: i in I;

      then (M . i) in (( doms F) . i) by A1;

      then

       A3: (M . i) in ( dom (F . i)) by A2, MSSUBFAM: 14;

      A is_transformable_to [|B, C|];

      then M in A by A1, MSSUBFAM: 17;

      then (F .. M) in [|B, C|] by CLOSURE1: 3;

      then ((F .. M) . i) in ( [|B, C|] . i) by A2;

      then ((F .. M) . i) in [:(B . i), (C . i):] by A2, PBOOLE:def 16;

      then

       A4: ((F . i) . (M . i)) in [:(B . i), (C . i):] by A2, PRALG_1:def 20;

      set z = ((F . i) . (M . i));

      (( Mpr2 F) . i) = ( pr2 (F . i)) by A2, Def2;

      

      then

       A5: ((( Mpr2 F) .. M) . i) = (( pr2 (F . i)) . (M . i)) by A2, PRALG_1:def 20

      .= (z `2 ) by A3, MCART_1:def 13;

      (( Mpr1 F) . i) = ( pr1 (F . i)) by A2, Def1;

      

      then ((( Mpr1 F) .. M) . i) = (( pr1 (F . i)) . (M . i)) by A2, PRALG_1:def 20

      .= (z `1 ) by A3, MCART_1:def 12;

      then z = [((( Mpr1 F) .. M) . i), ((( Mpr2 F) .. M) . i)] by A4, A5, MCART_1: 21;

      hence thesis by A2, PRALG_1:def 20;

    end;

    begin

    registration

      let S be non empty ManySortedSign;

      cluster the Sorts of ( Trivial_Algebra S) -> finite-yielding non-empty;

      coherence

      proof

        ex A be ManySortedSet of the carrier of S st {A} = (the carrier of S --> { 0 }) by Th5;

        hence thesis by MSAFREE2:def 12;

      end;

    end

    registration

      let S be non empty ManySortedSign;

      cluster ( Trivial_Algebra S) -> finite-yielding non-empty;

      coherence ;

    end

    theorem :: MSUALG_9:24

    

     Th24: for A be non-empty MSAlgebra over S holds for F be ManySortedFunction of A, ( Trivial_Algebra S) holds for o be OperSymbol of S holds for x be Element of ( Args (o,A)) holds ((F . ( the_result_sort_of o)) . (( Den (o,A)) . x)) = 0 & (( Den (o,( Trivial_Algebra S))) . (F # x)) = 0

    proof

      let A be non-empty MSAlgebra over S, F be ManySortedFunction of A, ( Trivial_Algebra S);

      let o be OperSymbol of S;

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

      set I = the carrier of S, SA = the Sorts of A, T = ( Trivial_Algebra S), ST = the Sorts of T;

      set r = ( the_result_sort_of o);

      consider i be object such that

       A1: i in I and

       A2: ( Result (o,T)) = (ST . i) by PBOOLE: 138;

      reconsider d = (( Den (o,A)) . x) as Element of (SA . r) by FUNCT_2: 15;

      consider XX be ManySortedSet of I such that

       A3: {XX} = (I --> { 0 }) by Th5;

      

       A4: ST = {XX} by A3, MSAFREE2:def 12;

      then

       A5: (ST . r) = { 0 } by A3;

      

      thus ((F . r) . (( Den (o,A)) . x)) = ((F . r) . d)

      .= 0 by A5, TARSKI:def 1;

      (ST . i) = { 0 } by A3, A4, A1, FUNCOP_1: 7;

      hence thesis by A2, TARSKI:def 1;

    end;

    theorem :: MSUALG_9:25

    

     Th25: for A be non-empty MSAlgebra over S holds for F be ManySortedFunction of A, ( Trivial_Algebra S) holds F is_epimorphism (A,( Trivial_Algebra S))

    proof

      let A be non-empty MSAlgebra over S, F be ManySortedFunction of A, ( Trivial_Algebra S);

      set I = the carrier of S;

      consider XX be ManySortedSet of I such that

       A1: {XX} = (I --> { 0 }) by Th5;

      thus F is_homomorphism (A,( Trivial_Algebra S))

      proof

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

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

        

        thus ((F . ( the_result_sort_of o)) . (( Den (o,A)) . x)) = 0 by Th24

        .= (( Den (o,( Trivial_Algebra S))) . (F # x)) by Th24;

      end;

      the Sorts of ( Trivial_Algebra S) = {XX} by A1, MSAFREE2:def 12;

      hence thesis by Th9;

    end;

    theorem :: MSUALG_9:26

    for A be MSAlgebra over S st ex X be ManySortedSet of the carrier of S st the Sorts of A = {X} holds (A,( Trivial_Algebra S)) are_isomorphic

    proof

      let A be MSAlgebra over S such that

       A1: ex X be ManySortedSet of the carrier of S st the Sorts of A = {X};

      set I = the carrier of S, SB = the Sorts of A, ST = the Sorts of ( Trivial_Algebra S);

      consider X be ManySortedSet of I such that

       A2: the Sorts of A = {X} by A1;

      set F = the ManySortedFunction of SB, ST;

      reconsider F1 = F as ManySortedFunction of {X}, ST by A2;

      take F;

      A is non-empty by A2;

      hence F is_epimorphism (A,( Trivial_Algebra S)) by Th25;

      hence F is_homomorphism (A,( Trivial_Algebra S));

      F1 is "1-1" by Th10;

      hence thesis;

    end;

    begin

    theorem :: MSUALG_9:27

    for A be non-empty MSAlgebra over S holds for C be MSCongruence of A holds C is ManySortedSubset of [|the Sorts of A, the Sorts of A|]

    proof

      let A be non-empty MSAlgebra over S, C be MSCongruence of A;

      set SF = the Sorts of A;

      let i be object such that

       A1: i in the carrier of S;

      (C . i) is Relation of (SF . i), (SF . i) by A1, MSUALG_4:def 1;

      then (C . i) c= [:(SF . i), (SF . i):];

      hence thesis by A1, PBOOLE:def 16;

    end;

    theorem :: MSUALG_9:28

    for A be non-empty MSAlgebra over S holds for R be Subset of ( CongrLatt A) holds for F be SubsetFamily of [|the Sorts of A, the Sorts of A|] st R = F holds ( meet |:F:|) is MSCongruence of A

    proof

      let A be non-empty MSAlgebra over S, R be Subset of ( CongrLatt A), F be SubsetFamily of [|the Sorts of A, the Sorts of A|] such that

       A1: R = F;

      set R0 = ( meet |:F:|), SF = the Sorts of A, I = the carrier of S;

      per cases ;

        suppose F is non empty;

        then

        reconsider F1 = F as non empty SubsetFamily of [|SF, SF|];

        

         A2: F1 c= the carrier of ( EqRelLatt SF)

        proof

          let q be object;

          assume q in F1;

          then q is MSCongruence of A by A1, MSUALG_5:def 6;

          hence thesis by MSUALG_5:def 5;

        end;

        then

         A3: R0 is MSEquivalence_Relation-like ManySortedRelation of SF by MSUALG_7: 8;

        reconsider R0 as ManySortedRelation of A by A2, MSUALG_7: 8;

        R0 is MSEquivalence-like by A3;

        then

        reconsider R0 as MSEquivalence-like ManySortedRelation of A;

        now

          let o be OperSymbol of S;

          let a,b be Element of ( Args (o,A)) such that

           A4: for n be Nat st n in ( dom a) holds [(a . n), (b . n)] in (R0 . (( the_arity_of o) /. n));

          set r = ( the_result_sort_of o);

          consider Q be Subset-Family of ( [|SF, SF|] . r) such that

           A5: Q = ( |:F1:| . r) and

           A6: (R0 . r) = ( Intersect Q) by MSSUBFAM:def 1;

          

           A7: Q = { (s . r) where s be Element of ( Bool [|SF, SF|]) : s in F1 } by A5, CLOSURE2: 14;

          now

            let Y be set;

            assume Y in Q;

            then

            consider s be Element of ( Bool [|SF, SF|]) such that

             A8: Y = (s . r) and

             A9: s in F1 by A7;

            reconsider s as MSCongruence of A by A1, A9, MSUALG_5:def 6;

            now

              let n be Nat such that

               A10: n in ( dom a);

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

              consider G be Subset-Family of ( [|SF, SF|] . t) such that

               A11: G = ( |:F1:| . t) and

               A12: (R0 . t) = ( Intersect G) by MSSUBFAM:def 1;

              G = { (j . t) where j be Element of ( Bool [|SF, SF|]) : j in F1 } by A11, CLOSURE2: 14;

              then

               A13: (s . t) in G by A9;

               [(a . n), (b . n)] in ( Intersect G) by A4, A10, A12;

              then [(a . n), (b . n)] in ( meet G) by A11, SETFAM_1:def 9;

              hence [(a . n), (b . n)] in (s . t) by A13, SETFAM_1:def 1;

            end;

            hence [(( Den (o,A)) . a), (( Den (o,A)) . b)] in Y by A8, MSUALG_4:def 4;

          end;

          then [(( Den (o,A)) . a), (( Den (o,A)) . b)] in ( meet Q) by A5, SETFAM_1:def 1;

          hence [(( Den (o,A)) . a), (( Den (o,A)) . b)] in (R0 . ( the_result_sort_of o)) by A5, A6, SETFAM_1:def 9;

        end;

        hence thesis by MSUALG_4:def 4;

      end;

        suppose F is empty;

        then |:F:| = ( EmptyMS I);

        then ( meet |:F:|) = [|the Sorts of A, the Sorts of A|] by MSSUBFAM: 41;

        hence thesis by MSUALG_5: 18;

      end;

    end;

    theorem :: MSUALG_9:29

    for A be non-empty MSAlgebra over S holds for C be MSCongruence of A st C = [|the Sorts of A, the Sorts of A|] holds the Sorts of ( QuotMSAlg (A,C)) = {the Sorts of A}

    proof

      let A be non-empty MSAlgebra over S, C be MSCongruence of A such that

       A1: C = [|the Sorts of A, the Sorts of A|];

      now

        let i be object;

        assume i in the carrier of S;

        then

        reconsider s = i as Element of S;

        

         A2: (C . s) = [:(the Sorts of A . s), (the Sorts of A . s):] by A1, PBOOLE:def 16

        .= ( nabla (the Sorts of A . s)) by EQREL_1:def 1;

        

        thus (the Sorts of ( QuotMSAlg (A,C)) . i) = ( Class (C . s)) by MSUALG_4:def 6

        .= {(the Sorts of A . s)} by A2, Th4

        .= ( {the Sorts of A} . i) by PZFMISC1:def 1;

      end;

      hence thesis;

    end;

    theorem :: MSUALG_9:30

    

     Th30: for A,B be non-empty MSAlgebra over S holds for F be ManySortedFunction of A, B st F is_homomorphism (A,B) holds (( MSHomQuot F) ** ( MSNat_Hom (A,( MSCng F)))) = F

    proof

      let A,B be non-empty MSAlgebra over S, F be ManySortedFunction of A, B such that

       A1: F is_homomorphism (A,B);

      now

        let i be object;

        assume i in the carrier of S;

        then

        reconsider s = i as SortSymbol of S;

        reconsider h = ( MSHomQuot (F,s)) as Function of (( Class ( MSCng F)) . s), (the Sorts of B . s);

        reconsider f = (h * ( MSNat_Hom (A,( MSCng F),s))) as Function of (the Sorts of A . s), (the Sorts of B . s);

        

         A2: for c be Element of (the Sorts of A . s) holds (f . c) = ((F . s) . c)

        proof

          let c be Element of (the Sorts of A . s);

          

          thus (f . c) = (h . (( MSNat_Hom (A,( MSCng F),s)) . c)) by FUNCT_2: 15

          .= (h . ( Class ((( MSCng F) . s),c))) by MSUALG_4:def 15

          .= (h . ( Class (( MSCng (F,s)),c))) by A1, MSUALG_4:def 18

          .= ((F . s) . c) by A1, MSUALG_4:def 19;

        end;

        

        thus ((( MSHomQuot F) ** ( MSNat_Hom (A,( MSCng F)))) . i) = ((( MSHomQuot F) . s) * (( MSNat_Hom (A,( MSCng F))) . s)) by MSUALG_3: 2

        .= (( MSHomQuot (F,s)) * (( MSNat_Hom (A,( MSCng F))) . s)) by MSUALG_4:def 20

        .= (( MSHomQuot (F,s)) * ( MSNat_Hom (A,( MSCng F),s))) by MSUALG_4:def 16

        .= (F . i) by A2, FUNCT_2: 63;

      end;

      hence thesis;

    end;

    theorem :: MSUALG_9:31

    

     Th31: for A be non-empty MSAlgebra over S holds for C be MSCongruence of A holds for s be SortSymbol of S holds for a be Element of (the Sorts of ( QuotMSAlg (A,C)) . s) holds ex x be Element of (the Sorts of A . s) st a = ( Class (C,x))

    proof

      let A be non-empty MSAlgebra over S, C be MSCongruence of A, s be SortSymbol of S, a be Element of (the Sorts of ( QuotMSAlg (A,C)) . s);

      a in (( Class C) . s);

      then a in ( Class (C . s)) by MSUALG_4:def 6;

      then

      consider t be object such that

       A1: t in (the Sorts of A . s) and

       A2: a = ( Class ((C . s),t)) by EQREL_1:def 3;

      reconsider t as Element of (the Sorts of A . s) by A1;

      take t;

      thus thesis by A2;

    end;

    theorem :: MSUALG_9:32

    for A be MSAlgebra over S holds for C1,C2 be MSEquivalence-like ManySortedRelation of A st C1 c= C2 holds for i be Element of S holds for x,y be Element of (the Sorts of A . i) st [x, y] in (C1 . i) holds ( Class (C1,x)) c= ( Class (C2,y)) & (A is non-empty implies ( Class (C1,y)) c= ( Class (C2,x)))

    proof

      let A be MSAlgebra over S, C1,C2 be MSEquivalence-like ManySortedRelation of A such that

       A1: C1 c= C2;

      let i be Element of S, x,y be Element of (the Sorts of A . i) such that

       A2: [x, y] in (C1 . i);

      ( field (C1 . i)) = (the Sorts of A . i) by ORDERS_1: 12;

      then

       A3: (C1 . i) is_transitive_in (the Sorts of A . i) by RELAT_2:def 16;

      

       A4: (C1 . i) c= (C2 . i) by A1;

      thus ( Class (C1,x)) c= ( Class (C2,y))

      proof

        let q be object;

        assume

         A5: q in ( Class (C1,x));

        then [q, x] in (C1 . i) by EQREL_1: 19;

        then [q, y] in (C1 . i) by A2, A3, A5, RELAT_2:def 8;

        hence thesis by A4, EQREL_1: 19;

      end;

      assume A is non-empty;

      then

      reconsider B = A as non-empty MSAlgebra over S;

      ( field (C1 . i)) = (the Sorts of A . i) by ORDERS_1: 12;

      then (C1 . i) is_symmetric_in (the Sorts of B . i) by RELAT_2:def 11;

      then

       A6: [y, x] in (C1 . i) by A2, RELAT_2:def 3;

      let q be object such that

       A7: q in ( Class (C1,y));

       [q, y] in (C1 . i) by A7, EQREL_1: 19;

      then [q, x] in (C1 . i) by A3, A7, A6, RELAT_2:def 8;

      hence thesis by A4, EQREL_1: 19;

    end;

    theorem :: MSUALG_9:33

    for A be non-empty MSAlgebra over S, C be MSCongruence of A holds for s be SortSymbol of S, x,y be Element of (the Sorts of A . s) holds ((( MSNat_Hom (A,C)) . s) . x) = ((( MSNat_Hom (A,C)) . s) . y) iff [x, y] in (C . s)

    proof

      let A be non-empty MSAlgebra over S, C be MSCongruence of A, s be SortSymbol of S, x,y be Element of (the Sorts of A . s);

      set f = (( MSNat_Hom (A,C)) . s), g = ( MSNat_Hom (A,C,s));

      

       A1: f = g by MSUALG_4:def 16;

      hereby

        assume

         A2: ((( MSNat_Hom (A,C)) . s) . x) = ((( MSNat_Hom (A,C)) . s) . y);

        ( Class ((C . s),x)) = (g . x) by MSUALG_4:def 15

        .= ( Class ((C . s),y)) by A1, A2, MSUALG_4:def 15;

        hence [x, y] in (C . s) by EQREL_1: 35;

      end;

      assume

       A3: [x, y] in (C . s);

      

      thus ((( MSNat_Hom (A,C)) . s) . x) = ( Class ((C . s),x)) by A1, MSUALG_4:def 15

      .= ( Class ((C . s),y)) by A3, EQREL_1: 35

      .= ((( MSNat_Hom (A,C)) . s) . y) by A1, MSUALG_4:def 15;

    end;

     Lm1:

    now

      let S be non empty non void ManySortedSign, A be non-empty MSAlgebra over S, C1,C2 be MSCongruence of A;

      let G be ManySortedFunction of ( QuotMSAlg (A,C1)), ( QuotMSAlg (A,C2)) such that

       A1: for i be Element of S holds for x be Element of (the Sorts of ( QuotMSAlg (A,C1)) . i) holds for xx be Element of (the Sorts of A . i) st x = ( Class (C1,xx)) holds ((G . i) . x) = ( Class (C2,xx));

      thus G is "onto"

      proof

        let i be set;

        set sL = the Sorts of ( QuotMSAlg (A,C1)), sP = the Sorts of ( QuotMSAlg (A,C2));

        assume i in the carrier of S;

        then

        reconsider s = i as SortSymbol of S;

        

         A2: ( dom (G . s)) = (sL . s) by FUNCT_2:def 1;

        ( rng (G . s)) c= (sP . s);

        hence ( rng (G . i)) c= (sP . i);

        let q be object;

        assume q in (sP . i);

        then q in ( Class (C2 . s)) by MSUALG_4:def 6;

        then

        consider a be object such that

         A3: a in (the Sorts of A . s) and

         A4: q = ( Class ((C2 . s),a)) by EQREL_1:def 3;

        reconsider a as Element of (the Sorts of A . s) by A3;

        ( Class ((C1 . s),a)) in ( Class (C1 . s)) by EQREL_1:def 3;

        then

        reconsider x = ( Class (C1,a)) as Element of (sL . s) by MSUALG_4:def 6;

        ((G . s) . x) = ( Class (C2,a)) by A1

        .= ( Class ((C2 . s),a));

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

      end;

    end;

    theorem :: MSUALG_9:34

    

     Th34: for A be non-empty MSAlgebra over S holds for C1,C2 be MSCongruence of A holds for G be ManySortedFunction of ( QuotMSAlg (A,C1)), ( QuotMSAlg (A,C2)) st for i be Element of S holds for x be Element of (the Sorts of ( QuotMSAlg (A,C1)) . i) holds for xx be Element of (the Sorts of A . i) st x = ( Class (C1,xx)) holds ((G . i) . x) = ( Class (C2,xx)) holds (G ** ( MSNat_Hom (A,C1))) = ( MSNat_Hom (A,C2))

    proof

      let A be non-empty MSAlgebra over S, C1,C2 be MSCongruence of A;

      set sL = the Sorts of ( QuotMSAlg (A,C1));

      let G be ManySortedFunction of ( QuotMSAlg (A,C1)), ( QuotMSAlg (A,C2)) such that

       A1: for i be Element of S holds for x be Element of (the Sorts of ( QuotMSAlg (A,C1)) . i) holds for xx be Element of (the Sorts of A . i) st x = ( Class (C1,xx)) holds ((G . i) . x) = ( Class (C2,xx));

      now

        let i be object;

        assume i in the carrier of S;

        then

        reconsider s = i as SortSymbol of S;

        

         A2: for c be Element of (the Sorts of A . s) holds (((G . s) * (( MSNat_Hom (A,C1)) . s)) . c) = ((( MSNat_Hom (A,C2)) . s) . c)

        proof

          let c be Element of (the Sorts of A . s);

          ( Class ((C1 . s),c)) in ( Class (C1 . s)) by EQREL_1:def 3;

          then

           A3: ( Class (C1,c)) is Element of (sL . s) by MSUALG_4:def 6;

          

          thus (((G . s) * (( MSNat_Hom (A,C1)) . s)) . c) = ((G . s) . ((( MSNat_Hom (A,C1)) . s) . c)) by FUNCT_2: 15

          .= ((G . s) . (( MSNat_Hom (A,C1,s)) . c)) by MSUALG_4:def 16

          .= ((G . s) . ( Class (C1,c))) by MSUALG_4:def 15

          .= ( Class (C2,c)) by A1, A3

          .= (( MSNat_Hom (A,C2,s)) . c) by MSUALG_4:def 15

          .= ((( MSNat_Hom (A,C2)) . s) . c) by MSUALG_4:def 16;

        end;

        

        thus ((G ** ( MSNat_Hom (A,C1))) . i) = ((G . s) * (( MSNat_Hom (A,C1)) . s)) by MSUALG_3: 2

        .= (( MSNat_Hom (A,C2)) . i) by A2, FUNCT_2: 63;

      end;

      hence thesis;

    end;

    theorem :: MSUALG_9:35

    

     Th35: for A be non-empty MSAlgebra over S holds for C1,C2 be MSCongruence of A holds for G be ManySortedFunction of ( QuotMSAlg (A,C1)), ( QuotMSAlg (A,C2)) st for i be Element of S holds for x be Element of (the Sorts of ( QuotMSAlg (A,C1)) . i) holds for xx be Element of (the Sorts of A . i) st x = ( Class (C1,xx)) holds ((G . i) . x) = ( Class (C2,xx)) holds G is_epimorphism (( QuotMSAlg (A,C1)),( QuotMSAlg (A,C2)))

    proof

      let A be non-empty MSAlgebra over S, C1,C2 be MSCongruence of A;

      ( MSNat_Hom (A,C2)) is_epimorphism (A,( QuotMSAlg (A,C2))) by MSUALG_4: 3;

      then

       A1: ( MSNat_Hom (A,C2)) is_homomorphism (A,( QuotMSAlg (A,C2)));

      let G be ManySortedFunction of ( QuotMSAlg (A,C1)), ( QuotMSAlg (A,C2)) such that

       A2: for i be Element of S holds for x be Element of (the Sorts of ( QuotMSAlg (A,C1)) . i) holds for xx be Element of (the Sorts of A . i) st x = ( Class (C1,xx)) holds ((G . i) . x) = ( Class (C2,xx));

      (G ** ( MSNat_Hom (A,C1))) = ( MSNat_Hom (A,C2)) by A2, Th34;

      hence G is_homomorphism (( QuotMSAlg (A,C1)),( QuotMSAlg (A,C2))) by A1, Th19, MSUALG_4: 3;

      thus thesis by A2, Lm1;

    end;

    theorem :: MSUALG_9:36

    for A,B be non-empty MSAlgebra over S holds for F be ManySortedFunction of A, B st F is_homomorphism (A,B) holds for C1 be MSCongruence of A st C1 c= ( MSCng F) holds ex H be ManySortedFunction of ( QuotMSAlg (A,C1)), B st H is_homomorphism (( QuotMSAlg (A,C1)),B) & F = (H ** ( MSNat_Hom (A,C1)))

    proof

      let A,B be non-empty MSAlgebra over S, F be ManySortedFunction of A, B such that

       A1: F is_homomorphism (A,B);

      ( MSHomQuot F) is_monomorphism (( QuotMSAlg (A,( MSCng F))),B) by A1, MSUALG_4: 4;

      then

       A2: ( MSHomQuot F) is_homomorphism (( QuotMSAlg (A,( MSCng F))),B);

      let C1 be MSCongruence of A such that

       A3: C1 c= ( MSCng F);

      set G = ( MSNat_Hom (A,C1)), I = the carrier of S, sQ = the Sorts of ( QuotMSAlg (A,C1)), sF = the Sorts of ( QuotMSAlg (A,( MSCng F)));

      defpred P[ object, object, object] means ex s be Element of I, xx be Element of (the Sorts of A . s) st $3 = s & $2 = ( Class (C1,xx)) & $1 = ( Class (( MSCng F),xx));

      

       A4: for i be object st i in I holds for x be object st x in (sQ . i) holds ex y be object st y in (sF . i) & P[y, x, i]

      proof

        let i be object;

        assume i in I;

        then

        reconsider s = i as Element of I;

        let x be object;

        assume x in (sQ . i);

        then

        consider x1 be Element of (the Sorts of A . s) such that

         A5: x = ( Class (C1,x1)) by Th31;

        take y = ( Class (( MSCng F),x1));

        y in ( Class (( MSCng F) . s)) by EQREL_1:def 3;

        hence y in (sF . i) by MSUALG_4:def 6;

        thus thesis by A5;

      end;

      consider C12 be ManySortedFunction of sQ, sF such that

       A6: for i be object st i in I holds ex f be Function of (sQ . i), (sF . i) st f = (C12 . i) & for x be object st x in (sQ . i) holds P[(f . x), x, i] from MSSUBFAM:sch 1( A4);

      reconsider H = (( MSHomQuot F) ** C12) as ManySortedFunction of ( QuotMSAlg (A,C1)), B;

      take H;

      

       A7: for i be Element of S holds for x be Element of (the Sorts of ( QuotMSAlg (A,C1)) . i) holds for xx be Element of (the Sorts of A . i) st x = ( Class (C1,xx)) holds ((C12 . i) . x) = ( Class (( MSCng F),xx))

      proof

        let i be Element of S, x be Element of (the Sorts of ( QuotMSAlg (A,C1)) . i), xx be Element of (the Sorts of A . i) such that

         A8: x = ( Class (C1,xx));

        consider f be Function of (sQ . i), (sF . i) such that

         A9: f = (C12 . i) and

         A10: for x be object st x in (sQ . i) holds P[(f . x), x, i] by A6;

        consider s be Element of I, x1 be Element of (the Sorts of A . s) such that

         A11: i = s and

         A12: x = ( Class (C1,x1)) and

         A13: (f . x) = ( Class (( MSCng F),x1)) by A10;

        xx in ( Class ((C1 . s),x1)) by A8, A12, EQREL_1: 23;

        then

         A14: [xx, x1] in (C1 . s) by EQREL_1: 19;

        (C1 . s) c= (( MSCng F) . s) by A3;

        then xx in ( Class ((( MSCng F) . s),x1)) by A14, EQREL_1: 19;

        hence thesis by A9, A11, A13, EQREL_1: 23;

      end;

      then C12 is_epimorphism (( QuotMSAlg (A,C1)),( QuotMSAlg (A,( MSCng F)))) by Th35;

      then C12 is_homomorphism (( QuotMSAlg (A,C1)),( QuotMSAlg (A,( MSCng F))));

      hence H is_homomorphism (( QuotMSAlg (A,C1)),B) by A2, MSUALG_3: 10;

       A15:

      now

        let i be object;

        assume i in the carrier of S;

        then

        reconsider s = i as SortSymbol of S;

        

         A16: for x be Element of (the Sorts of A . s) holds (((C12 . s) * (G . s)) . x) = ((( MSNat_Hom (A,( MSCng F))) . s) . x)

        proof

          let x be Element of (the Sorts of A . s);

          ( Class ((C1 . s),x)) in ( Class (C1 . s)) by EQREL_1:def 3;

          then

           A17: ( Class (C1,x)) in (( Class C1) . s) by MSUALG_4:def 6;

          

          thus (((C12 . s) * (G . s)) . x) = ((C12 . s) . ((G . s) . x)) by FUNCT_2: 15

          .= ((C12 . s) . (( MSNat_Hom (A,C1,s)) . x)) by MSUALG_4:def 16

          .= ((C12 . s) . ( Class (C1,x))) by MSUALG_4:def 15

          .= ( Class (( MSCng F),x)) by A7, A17

          .= (( MSNat_Hom (A,( MSCng F),s)) . x) by MSUALG_4:def 15

          .= ((( MSNat_Hom (A,( MSCng F))) . s) . x) by MSUALG_4:def 16;

        end;

        

        thus ((C12 ** G) . i) = ((C12 . s) * (G . s)) by MSUALG_3: 2

        .= (( MSNat_Hom (A,( MSCng F))) . i) by A16, FUNCT_2: 63;

      end;

      

      thus F = (( MSHomQuot F) ** ( MSNat_Hom (A,( MSCng F)))) by A1, Th30

      .= (( MSHomQuot F) ** (C12 ** G)) by A15, PBOOLE: 3

      .= (H ** ( MSNat_Hom (A,C1))) by PBOOLE: 140;

    end;