pralg_3.miz



    begin

    reserve I for non empty set,

J for ManySortedSet of I,

S for non void non empty ManySortedSign,

i for Element of I,

c for set,

A for MSAlgebra-Family of I, S,

EqR for Equivalence_Relation of I,

U0,U1,U2 for MSAlgebra over S,

s for SortSymbol of S,

o for OperSymbol of S,

f for Function;

    registration

      let I be set, S;

      let AF be MSAlgebra-Family of I, S;

      cluster ( product AF) -> non-empty;

      coherence by MSUALG_1:def 3;

    end

    registration

      let X be with_non-empty_elements set;

      cluster ( id X) -> non-empty;

      coherence ;

    end

    theorem :: PRALG_3:1

    

     Th1: for f,F be Function, A be set st f in ( product F) holds (f | A) in ( product (F | A))

    proof

      let f,F be Function, A be set;

      assume

       A1: f in ( product F);

      then ( dom f) = ( dom F) by CARD_3: 9;

      

      then

       A2: ( dom (f | A)) = (( dom F) /\ A) by RELAT_1: 61

      .= ( dom (F | A)) by RELAT_1: 61;

      for x be object st x in ( dom (F | A)) holds ((f | A) . x) in ((F | A) . x)

      proof

        let x be object;

        assume

         A3: x in ( dom (F | A));

        then x in (( dom F) /\ A) by RELAT_1: 61;

        then

         A4: x in ( dom F) by XBOOLE_0:def 4;

        ((F | A) . x) = (F . x) & ((f | A) . x) = (f . x) by A2, A3, FUNCT_1: 47;

        hence thesis by A1, A4, CARD_3: 9;

      end;

      hence thesis by A2, CARD_3: 9;

    end;

    theorem :: PRALG_3:2

    

     Th2: for A be MSAlgebra-Family of I, S, s be SortSymbol of S, a be non empty Subset of I, Aa be MSAlgebra-Family of a, S st (A | a) = Aa holds ( Carrier (Aa,s)) = (( Carrier (A,s)) | a)

    proof

      let A be MSAlgebra-Family of I, S, s be SortSymbol of S, a be non empty Subset of I, Aa be MSAlgebra-Family of a, S such that

       A1: (A | a) = Aa;

      ( dom (( Carrier (A,s)) | a)) = (( dom ( Carrier (A,s))) /\ a) by RELAT_1: 61

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

      .= a by XBOOLE_1: 28;

      then

      reconsider Cas = (( Carrier (A,s)) | a) as ManySortedSet of a by PARTFUN1:def 2;

      for i be object st i in a holds (( Carrier (Aa,s)) . i) = (Cas . i)

      proof

        let i be object;

        assume

         A2: i in a;

        then

        reconsider i9 = i as Element of a;

        reconsider i99 = i9 as Element of I;

        

         A3: (Aa . i9) = (A . i9) & ex U1 be MSAlgebra over S st U1 = (A . i99) & (( Carrier (A,s)) . i99) = (the Sorts of U1 . s) by A1, FUNCT_1: 49, PRALG_2:def 9;

        ex U0 be MSAlgebra over S st U0 = (Aa . i) & (( Carrier (Aa,s)) . i) = (the Sorts of U0 . s) by A2, PRALG_2:def 9;

        hence thesis by A3, FUNCT_1: 49;

      end;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: PRALG_3:3

    

     Th3: for i be set, I be non empty set, EqR be Equivalence_Relation of I, c1,c2 be Element of ( Class EqR) st i in c1 & i in c2 holds c1 = c2

    proof

      let i be set, I be non empty set, EqR be Equivalence_Relation of I, c1,c2 be Element of ( Class EqR) such that

       A1: i in c1 and

       A2: i in c2;

      consider x1 be object such that x1 in I and

       A3: c1 = ( Class (EqR,x1)) by EQREL_1:def 3;

      

       A4: [i, x1] in EqR by A1, A3, EQREL_1: 19;

      consider x2 be object such that x2 in I and

       A5: c2 = ( Class (EqR,x2)) by EQREL_1:def 3;

       [i, x2] in EqR by A2, A5, EQREL_1: 19;

      

      then ( Class (EqR,x2)) = ( Class (EqR,i)) by A1, EQREL_1: 35

      .= c1 by A1, A3, A4, EQREL_1: 35;

      hence thesis by A5;

    end;

    

     Lm1: for f be Function, x be set st x in ( product f) holds x is Function;

    theorem :: PRALG_3:4

    for D be non empty set holds for F be ManySortedFunction of D holds for C be with_common_domain functional non empty set st C = ( rng F) holds for d be Element of D, e be set st e in ( DOM C) holds ((F . d) . e) = ((( commute F) . e) . d)

    proof

      let D be non empty set;

      let F be ManySortedFunction of D;

      set E = ( union the set of all ( rng (F . d9)) where d9 be Element of D);

      reconsider F9 = F as Function;

      let C be with_common_domain functional non empty set such that

       A1: C = ( rng F);

      

       A2: ( rng F9) c= ( Funcs (( DOM C),E))

      proof

        let x be object;

        assume x in ( rng F9);

        then

        consider d9 be object such that

         A3: d9 in ( dom F) and

         A4: (F . d9) = x by FUNCT_1:def 3;

        reconsider d9 as Element of D by A3;

        consider Fd be Function such that

         A5: Fd = (F . d9);

        

         A6: ( rng Fd) c= E

        proof

          

           A7: ( rng Fd) in the set of all ( rng (F . d99)) where d99 be Element of D by A5;

          let x1 be object;

          assume x1 in ( rng Fd);

          hence thesis by A7, TARSKI:def 4;

        end;

        (F . d9) in ( rng F) by A3, FUNCT_1:def 3;

        then ( dom Fd) = ( DOM C) by A1, A5, CARD_3: 108;

        hence thesis by A4, A5, A6, FUNCT_2:def 2;

      end;

      let d be Element of D, e be set;

      assume

       A8: e in ( DOM C);

      ( dom F9) = D by PARTFUN1:def 2;

      then F in ( Funcs (D,( Funcs (( DOM C),E)))) by A2, FUNCT_2:def 2;

      hence thesis by A8, FUNCT_6: 56;

    end;

    begin

    definition

      let S, U0;

      let o be OperSymbol of S;

      :: PRALG_3:def1

      func const (o,U0) -> set equals (( Den (o,U0)) . {} );

      correctness ;

    end

    theorem :: PRALG_3:5

    

     Th5: ( the_arity_of o) = {} & ( Result (o,U0)) <> {} implies ( const (o,U0)) in ( Result (o,U0))

    proof

      assume that

       A1: ( the_arity_of o) = {} and

       A2: ( Result (o,U0)) <> {} ;

      ( dom ( Den (o,U0))) = ( Args (o,U0)) by A2, FUNCT_2:def 1

      .= { {} } by A1, PRALG_2: 4;

      then {} in ( dom ( Den (o,U0))) by TARSKI:def 1;

      then (( Den (o,U0)) . {} ) in ( rng ( Den (o,U0))) by FUNCT_1:def 3;

      hence thesis;

    end;

    theorem :: PRALG_3:6

    (the Sorts of U0 . s) <> {} implies ( Constants (U0,s)) = { ( const (o,U0)) where o be Element of the carrier' of S : ( the_result_sort_of o) = s & ( the_arity_of o) = {} }

    proof

      assume

       A1: (the Sorts of U0 . s) <> {} ;

      thus ( Constants (U0,s)) c= { ( const (o,U0)) where o be Element of the carrier' of S : ( the_result_sort_of o) = s & ( the_arity_of o) = {} }

      proof

        let x be object;

        assume

         A2: x in ( Constants (U0,s));

        ex A be non empty set st A = (the Sorts of U0 . s) & ( Constants (U0,s)) = { a where a be Element of A : ex o be OperSymbol of S st (the Arity of S . o) = {} & (the ResultSort of S . o) = s & a in ( rng ( Den (o,U0))) } by A1, MSUALG_2:def 3;

        then

        consider A be non empty set such that A = (the Sorts of U0 . s) and

         A3: x in { a where a be Element of A : ex o be OperSymbol of S st (the Arity of S . o) = {} & (the ResultSort of S . o) = s & a in ( rng ( Den (o,U0))) } by A2;

        consider a be Element of A such that

         A4: a = x and

         A5: ex o be OperSymbol of S st (the Arity of S . o) = {} & (the ResultSort of S . o) = s & a in ( rng ( Den (o,U0))) by A3;

        consider o1 be OperSymbol of S such that

         A6: (the Arity of S . o1) = {} and

         A7: (the ResultSort of S . o1) = s and

         A8: a in ( rng ( Den (o1,U0))) by A5;

        

         A9: ex x1 be object st x1 in ( dom ( Den (o1,U0))) & a = (( Den (o1,U0)) . x1) by A8, FUNCT_1:def 3;

        

         A10: ( the_result_sort_of o1) = s by A7, MSUALG_1:def 2;

        

         A11: ( the_arity_of o1) = {} by A6, MSUALG_1:def 1;

        then ( Args (o1,U0)) = { {} } by PRALG_2: 4;

        then x = ( const (o1,U0)) by A4, A9, TARSKI:def 1;

        hence thesis by A10, A11;

      end;

      let x be object;

      assume x in { ( const (o,U0)) where o be Element of the carrier' of S : ( the_result_sort_of o) = s & ( the_arity_of o) = {} };

      then

      consider o be Element of the carrier' of S such that

       A12: x = ( const (o,U0)) and

       A13: ( the_result_sort_of o) = s and

       A14: ( the_arity_of o) = {} ;

      o in the carrier' of S;

      then

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

      

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

      .= (the Sorts of U0 . (the ResultSort of S . o)) by A15, FUNCT_1: 13

      .= (the Sorts of U0 . s) by A13, MSUALG_1:def 2;

      thus x in ( Constants (U0,s))

      proof

        

         A17: ex o be OperSymbol of S st (the Arity of S . o) = {} & (the ResultSort of S . o) = s & x in ( rng ( Den (o,U0)))

        proof

          take o;

          ( Args (o,U0)) = ( dom ( Den (o,U0))) & ( Args (o,U0)) = { {} } by A1, A14, A16, FUNCT_2:def 1, PRALG_2: 4;

          then {} in ( dom ( Den (o,U0))) by TARSKI:def 1;

          hence thesis by A12, A13, A14, FUNCT_1:def 3, MSUALG_1:def 1, MSUALG_1:def 2;

        end;

        consider A be non empty set such that

         A18: A = (the Sorts of U0 . s) and

         A19: ( Constants (U0,s)) = { a where a be Element of A : ex o be OperSymbol of S st (the Arity of S . o) = {} & (the ResultSort of S . o) = s & a in ( rng ( Den (o,U0))) } by A1, MSUALG_2:def 3;

        x is Element of A by A12, A14, A16, A18, Th5;

        hence thesis by A19, A17;

      end;

    end;

    theorem :: PRALG_3:7

    

     Th7: ( the_arity_of o) = {} implies (( commute ( OPER A)) . o) in ( Funcs (I,( Funcs ( { {} },( union the set of all ( Result (o,(A . i9))) where i9 be Element of I)))))

    proof

      set f = (( commute ( OPER A)) . o);

      set C = ( union the set of all ( Result (o,(A . i9))) where i9 be Element of I);

      ( commute ( OPER A)) in ( Funcs (the carrier' of S,( Funcs (I,( rng ( uncurry ( OPER A))))))) by PRALG_2: 6;

      then

       A1: ex f1 be Function st ( commute ( OPER A)) = f1 & ( dom f1) = the carrier' of S & ( rng f1) c= ( Funcs (I,( rng ( uncurry ( OPER A))))) by FUNCT_2:def 2;

      then f in ( rng ( commute ( OPER A))) by FUNCT_1:def 3;

      then

       A2: ex fb be Function st fb = f & ( dom fb) = I & ( rng fb) c= ( rng ( uncurry ( OPER A))) by A1, FUNCT_2:def 2;

      assume

       A3: ( the_arity_of o) = {} ;

      now

        let x be object;

        assume x in ( rng f);

        then

        consider a be object such that

         A4: a in ( dom f) and

         A5: (f . a) = x by FUNCT_1:def 3;

        f = (A ?. o);

        then

        reconsider x9 = x as Function by A5;

        reconsider a as Element of I by A2, A4;

        

         A6: x9 = ((A ?. o) . a) by A5

        .= ( Den (o,(A . a))) by PRALG_2: 7;

        

        then

         A7: ( dom x9) = ( Args (o,(A . a))) by FUNCT_2:def 1

        .= { {} } by A3, PRALG_2: 4;

        now

          let c be object;

          assume c in ( rng x9);

          then

          consider b be object such that

           A8: b in ( dom x9) and

           A9: (x9 . b) = c by FUNCT_1:def 3;

          (x9 . b) = ( const (o,(A . a))) by A6, A7, A8, TARSKI:def 1;

          then

           A10: c is Element of ( Result (o,(A . a))) by A3, A9, Th5;

          ( Result (o,(A . a))) in the set of all ( Result (o,(A . i9))) where i9 be Element of I;

          hence c in C by A10, TARSKI:def 4;

        end;

        then ( rng x9) c= C;

        hence x in ( Funcs ( { {} },C)) by A7, FUNCT_2:def 2;

      end;

      then ( rng f) c= ( Funcs ( { {} },C));

      hence thesis by A2, FUNCT_2:def 2;

    end;

    theorem :: PRALG_3:8

    

     Th8: ( the_arity_of o) = {} implies ( const (o,( product A))) in ( Funcs (I,( union the set of all ( Result (o,(A . i9))) where i9 be Element of I)))

    proof

      set g = (( commute ( OPER A)) . o);

      set C = ( union the set of all ( Result (o,(A . i9))) where i9 be Element of I);

      assume

       A1: ( the_arity_of o) = {} ;

      then

       A2: g in ( Funcs (I,( Funcs ( { {} },C)))) by Th7;

      reconsider g as Function;

      (( OPS A) . o) = ( IFEQ (( the_arity_of o), {} ,( commute (A ?. o)),( Commute ( Frege (A ?. o))))) by PRALG_2:def 13

      .= ( commute (A ?. o)) by A1, FUNCOP_1:def 8;

      then

       A3: ( const (o,( product A))) = (( commute g) . {} ) by MSUALG_1:def 6;

      ( commute g) in ( Funcs ( { {} },( Funcs (I,C)))) by A2, FUNCT_6: 55;

      then

      consider g1 be Function such that

       A4: g1 = ( commute g) and

       A5: ( dom g1) = { {} } and

       A6: ( rng g1) c= ( Funcs (I,C)) by FUNCT_2:def 2;

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

      then (g1 . {} ) in ( rng g1) by A5, FUNCT_1:def 3;

      hence thesis by A3, A4, A6;

    end;

    registration

      let S, I, o, A;

      cluster ( const (o,( product A))) -> Relation-like Function-like;

      coherence

      proof

        ( const (o,( product A))) is Function

        proof

          per cases ;

            suppose ( the_arity_of o) = {} ;

            then ( const (o,( product A))) in ( Funcs (I,( union the set of all ( Result (o,(A . i9))) where i9 be Element of I))) by Th8;

            then ex g be Function st g = ( const (o,( product A))) & ( dom g) = I & ( rng g) c= ( union the set of all ( Result (o,(A . i9))) where i9 be Element of I) by FUNCT_2:def 2;

            hence thesis;

          end;

            suppose

             A1: ( the_arity_of o) <> {} ;

            ( dom (the Sorts of ( product A) * ( the_arity_of o))) = ( dom ( the_arity_of o)) by PRALG_2: 3;

            then

             A2: ( dom (the Sorts of ( product A) * ( the_arity_of o))) <> ( dom {} ) by A1;

            ( dom ( Den (o,( product A)))) = ( Args (o,( product A))) by FUNCT_2:def 1

            .= ( product (the Sorts of ( product A) * ( the_arity_of o))) by PRALG_2: 3;

            then not {} in ( dom ( Den (o,( product A)))) by A2, CARD_3: 9;

            hence thesis by FUNCT_1:def 2;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: PRALG_3:9

    

     Th9: for o be OperSymbol of S st ( the_arity_of o) = {} holds (( const (o,( product A))) . i) = ( const (o,(A . i)))

    proof

      let o be OperSymbol of S such that

       A1: ( the_arity_of o) = {} ;

      set f = (( commute ( OPER A)) . o), C = ( union the set of all ( Result (o,(A . i9))) where i9 be Element of I);

      

       A2: f in ( Funcs (I,( Funcs ( { {} },C)))) by A1, Th7;

      (( OPS A) . o) = ( IFEQ (( the_arity_of o), {} ,( commute (A ?. o)),( Commute ( Frege (A ?. o))))) by PRALG_2:def 13

      .= ( commute (A ?. o)) by A1, FUNCOP_1:def 8;

      then

       A3: ( const (o,( product A))) = (( commute f) . {} ) by MSUALG_1:def 6;

      

       A4: {} in { {} } by TARSKI:def 1;

      ( const (o,(A . i))) = (((A ?. o) . i) . {} ) by PRALG_2: 7

      .= (( const (o,( product A))) . i) by A2, A3, A4, FUNCT_6: 56;

      hence thesis;

    end;

    theorem :: PRALG_3:10

    ( the_arity_of o) = {} & ( dom f) = I & (for i be Element of I holds (f . i) = ( const (o,(A . i)))) implies f = ( const (o,( product A)))

    proof

      assume that

       A1: ( the_arity_of o) = {} and

       A2: ( dom f) = I and

       A3: for i be Element of I holds (f . i) = ( const (o,(A . i)));

       A4:

      now

        let a be object;

        assume a in I;

        then

        reconsider a9 = a as Element of I;

        

        thus (f . a) = ( const (o,(A . a9))) by A3

        .= (( const (o,( product A))) . a) by A1, Th9;

      end;

      set C = ( union the set of all ( Result (o,(A . i9))) where i9 be Element of I);

      ( const (o,( product A))) in ( Funcs (I,C)) by A1, Th8;

      then ex g2 be Function st g2 = ( const (o,( product A))) & ( dom g2) = I & ( rng g2) c= C by FUNCT_2:def 2;

      hence thesis by A2, A4;

    end;

    theorem :: PRALG_3:11

    

     Th11: for e be Element of ( Args (o,U1)) st e = {} & ( the_arity_of o) = {} & ( Args (o,U1)) <> {} & ( Args (o,U2)) <> {} holds for F be ManySortedFunction of U1, U2 holds (F # e) = {}

    proof

      let e be Element of ( Args (o,U1)) such that

       A1: e = {} and

       A2: ( the_arity_of o) = {} and

       A3: ( Args (o,U1)) <> {} & ( Args (o,U2)) <> {} ;

      reconsider e1 = e as Function by A1;

      let F be ManySortedFunction of U1, U2;

      

       A4: ( dom (F * ( the_arity_of o))) = {} by A2;

      then ( rng (F * ( the_arity_of o))) = {} by RELAT_1: 42;

      then (F * ( the_arity_of o)) is Function of {} , {} by A4, FUNCT_2: 1;

      then

       A5: e1 in ( product ( doms (F * ( the_arity_of o)))) by A1, CARD_3: 10, FUNCT_6: 23, TARSKI:def 1;

      

       A6: (F # e) = (( Frege (F * ( the_arity_of o))) . e) by A3, MSUALG_3:def 5

      .= ((F * ( the_arity_of o)) .. e1) by A5, PRALG_2:def 2;

      then

      reconsider fn = (F # e) as Function;

      ( dom fn) = ( {} /\ ( dom e1)) by A4, A6, PRALG_1:def 19;

      hence thesis;

    end;

    begin

    theorem :: PRALG_3:12

    

     Th12: for U1,U2 be non-empty MSAlgebra over S holds for F be ManySortedFunction of U1, U2 holds for x be Element of ( Args (o,U1)) holds x in ( product ( doms (F * ( the_arity_of o))))

    proof

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

      let F be ManySortedFunction of U1, U2;

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

      x in ( Args (o,U1));

      then

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

      

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

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

      then

       A3: ( rng ( the_arity_of o)) c= ( dom F);

       A4:

      now

        let n be object;

        assume n in ( dom ( doms (F * ( the_arity_of o))));

        then n in ( dom (F * ( the_arity_of o))) by FUNCT_6:def 2;

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

        hence n in ( dom x) by A3, A2, RELAT_1: 27;

      end;

      

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

       A6:

      now

        let n be object;

        assume

         A7: n in ( dom ( doms (F * ( the_arity_of o))));

        then

         A8: n in ( dom ( the_arity_of o)) by A2, A4;

        then (( the_arity_of o) . n) in ( rng ( the_arity_of o)) by FUNCT_1:def 3;

        then

        reconsider s1 = (( the_arity_of o) . n) as Element of the carrier of S;

        

         A9: n in ( dom (F * ( the_arity_of o))) by A3, A8, RELAT_1: 27;

        then ((F * ( the_arity_of o)) . n) = (F . s1) by FUNCT_1: 12;

        

        then

         A10: (( doms (F * ( the_arity_of o))) . n) = ( dom (F . s1)) by A9, FUNCT_6: 22

        .= (the Sorts of U1 . s1) by FUNCT_2:def 1;

        n in ( dom (the Sorts of U1 * ( the_arity_of o))) by A5, A4, A7;

        then (x . n) in ((the Sorts of U1 * ( the_arity_of o)) . n) by A1, CARD_3: 9;

        hence (x . n) in (( doms (F * ( the_arity_of o))) . n) by A5, A4, A7, A10, FUNCT_1: 12;

      end;

      now

        let n be object;

        assume n in ( dom x);

        then

         A11: n in ( dom (F * ( the_arity_of o))) by A3, A2, RELAT_1: 27;

        n in ( dom (F * ( the_arity_of o))) by A11;

        hence n in ( dom ( doms (F * ( the_arity_of o)))) by FUNCT_6:def 2;

      end;

      then

       A12: ( dom x) c= ( dom ( doms (F * ( the_arity_of o))));

      ( dom ( doms (F * ( the_arity_of o)))) c= ( dom x) by A4;

      then ( dom x) = ( dom ( doms (F * ( the_arity_of o)))) by A12;

      hence thesis by A6, CARD_3: 9;

    end;

    theorem :: PRALG_3:13

    

     Th13: for U1,U2 be non-empty MSAlgebra over S holds for F be ManySortedFunction of U1, U2 holds for x be Element of ( Args (o,U1)) holds for n be set st n in ( dom ( the_arity_of o)) holds ((F # x) . n) = ((F . (( the_arity_of o) /. n)) . (x . n))

    proof

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

      let F be ManySortedFunction of U1, U2;

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

      let n be set such that

       A1: n in ( dom ( the_arity_of o));

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

      then

       a1: ( rng ( the_arity_of o)) c= ( dom F);

      then

       A2: n in ( dom (F * ( the_arity_of o))) by A1, RELAT_1: 27;

      

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

      ( dom (F * ( the_arity_of o))) = ( dom ( the_arity_of o)) by a1, RELAT_1: 27;

      

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

      .= ( dom ( the_arity_of o)) by B2;

      then

       a2: n in ( dom ((F * ( the_arity_of o)) .. x)) by A1;

      

       A3: x in ( product ( doms (F * ( the_arity_of o)))) by Th12;

      

      thus ((F # x) . n) = ((( Frege (F * ( the_arity_of o))) . x) . n) by MSUALG_3:def 5

      .= (((F * ( the_arity_of o)) .. x) . n) by A3, PRALG_2:def 2

      .= (((F * ( the_arity_of o)) . n) . (x . n)) by a2, PRALG_1:def 19

      .= ((F . (( the_arity_of o) . n)) . (x . n)) by A2, FUNCT_1: 12

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

    end;

    theorem :: PRALG_3:14

    

     Th14: for x be Element of ( Args (o,( product A))) holds x in ( Funcs (( dom ( the_arity_of o)),( Funcs (I,( union the set of all (the Sorts of (A . i9) . s9) where i9 be Element of I, s9 be Element of the carrier of S)))))

    proof

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

      set C = ( union the set of all (the Sorts of (A . i9) . s9) where i9 be Element of I, s9 be Element of the carrier of S);

      consider x1 be Function such that

       A1: x1 = x;

      x in ( Args (o,( product A)));

      then

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

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

      then

       A3: ( rng ( the_arity_of o)) c= ( dom ( SORTS A));

      now

        let c be object;

        assume c in ( rng x1);

        then

        consider n be object such that

         A4: n in ( dom x1) and

         A5: (x1 . n) = c by FUNCT_1:def 3;

        

         A6: n in ( dom (( SORTS A) * ( the_arity_of o))) by A2, A1, A4, CARD_3: 9;

        then n in ( dom ( the_arity_of o)) by A3, RELAT_1: 27;

        then (( the_arity_of o) . n) in ( rng ( the_arity_of o)) by FUNCT_1:def 3;

        then

        reconsider s1 = (( the_arity_of o) . n) as Element of the carrier of S;

        (x1 . n) in ((( SORTS A) * ( the_arity_of o)) . n) by A2, A1, A6, CARD_3: 9;

        then (x1 . n) in (( SORTS A) . s1) by A6, FUNCT_1: 12;

        then (x1 . n) in ( product ( Carrier (A,s1))) by PRALG_2:def 10;

        then

        consider g be Function such that

         A7: g = (x1 . n) and

         A8: ( dom g) = ( dom ( Carrier (A,s1))) and

         A9: for i9 be object st i9 in ( dom ( Carrier (A,s1))) holds (g . i9) in (( Carrier (A,s1)) . i9) by CARD_3:def 5;

        now

          let c1 be object;

          assume c1 in ( rng g);

          then

          consider i1 be object such that

           A10: i1 in ( dom g) and

           A11: (g . i1) = c1 by FUNCT_1:def 3;

          reconsider i1 as Element of I by A8, A10;

          ex U0 be MSAlgebra over S st U0 = (A . i1) & (( Carrier (A,s1)) . i1) = (the Sorts of U0 . s1) by PRALG_2:def 9;

          then

           A12: (g . i1) in (the Sorts of (A . i1) . s1) by A8, A9, A10;

          (the Sorts of (A . i1) . s1) in the set of all (the Sorts of (A . i9) . s9) where i9 be Element of I, s9 be Element of the carrier of S;

          hence c1 in C by A11, A12, TARSKI:def 4;

        end;

        then

         A13: ( rng g) c= C;

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

        hence c in ( Funcs (I,C)) by A5, A7, A13, FUNCT_2:def 2;

      end;

      then

       A14: ( rng x1) c= ( Funcs (I,C));

      ( dom x) = ( dom (( SORTS A) * ( the_arity_of o))) by A2, CARD_3: 9

      .= ( dom ( the_arity_of o)) by A3, RELAT_1: 27;

      hence thesis by A1, A14, FUNCT_2:def 2;

    end;

    theorem :: PRALG_3:15

    

     Th15: for x be Element of ( Args (o,( product A))) holds for n be set st n in ( dom ( the_arity_of o)) holds (x . n) in ( product ( Carrier (A,(( the_arity_of o) /. n))))

    proof

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

      let n be set such that

       A1: n in ( dom ( the_arity_of o));

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

      then ( rng ( the_arity_of o)) c= ( dom ( SORTS A));

      then

       A2: n in ( dom (( SORTS A) * ( the_arity_of o))) by A1, RELAT_1: 27;

      x in ( Args (o,( product A)));

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

      then (x . n) in ((( SORTS A) * ( the_arity_of o)) . n) by A2, CARD_3: 9;

      then (x . n) in (( SORTS A) . (( the_arity_of o) . n)) by A2, FUNCT_1: 12;

      then (x . n) in (( SORTS A) . (( the_arity_of o) /. n)) by A1, PARTFUN1:def 6;

      hence thesis by PRALG_2:def 10;

    end;

    theorem :: PRALG_3:16

    

     Th16: for i be Element of I holds for n be set st n in ( dom ( the_arity_of o)) holds for s be SortSymbol of S st s = (( the_arity_of o) . n) holds for y be Element of ( Args (o,( product A))) holds for g be Function st g = (y . n) holds (g . i) in (the Sorts of (A . i) . s)

    proof

      let i be Element of I;

      let n be set;

      assume n in ( dom ( the_arity_of o));

      then

       A1: n in ( dom (the Sorts of ( product A) * ( the_arity_of o))) by PRALG_2: 3;

      let s be SortSymbol of S such that

       A2: s = (( the_arity_of o) . n);

      let y be Element of ( Args (o,( product A)));

      y in ( Args (o,( product A)));

      then

       A3: y in ( product (the Sorts of ( product A) * ( the_arity_of o))) by PRALG_2: 3;

      let g be Function;

      assume g = (y . n);

      then g in ((the Sorts of ( product A) * ( the_arity_of o)) . n) by A1, A3, CARD_3: 9;

      then g in (the Sorts of ( product A) . s) by A2, A1, FUNCT_1: 12;

      then

       A4: g in ( product ( Carrier (A,s))) by PRALG_2:def 10;

      i in I;

      then

       A5: i in ( dom ( Carrier (A,s))) by PARTFUN1:def 2;

      ex U0 be MSAlgebra over S st U0 = (A . i) & (( Carrier (A,s)) . i) = (the Sorts of U0 . s) by PRALG_2:def 9;

      hence thesis by A5, A4, CARD_3: 9;

    end;

    theorem :: PRALG_3:17

    

     Th17: for y be Element of ( Args (o,( product A))) st ( the_arity_of o) <> {} holds ( commute y) in ( product ( doms (A ?. o)))

    proof

      let y be Element of ( Args (o,( product A)));

      set D = ( union the set of all (the Sorts of (A . i9) . s9) where i9 be Element of I, s9 be Element of the carrier of S);

      

       A1: y in ( Funcs (( dom ( the_arity_of o)),( Funcs (I,D)))) by Th14;

      assume ( the_arity_of o) <> {} ;

      then ( commute y) in ( Funcs (I,( Funcs (( dom ( the_arity_of o)),D)))) by A1, FUNCT_6: 55;

      then

       A2: ex f be Function st f = ( commute y) & ( dom f) = I & ( rng f) c= ( Funcs (( dom ( the_arity_of o)),D)) by FUNCT_2:def 2;

       A3:

      now

        let i1 be object;

        assume i1 in ( dom ( doms (A ?. o)));

        then

        reconsider ii = i1 as Element of I by PRALG_2: 11;

         A4:

        now

          let n be object;

          assume

           A5: n in ( dom (the Sorts of (A . ii) * ( the_arity_of o)));

          then

           A6: n in ( dom ( the_arity_of o)) by PRALG_2: 3;

          then (( the_arity_of o) . n) in ( rng ( the_arity_of o)) by FUNCT_1:def 3;

          then

          reconsider s1 = (( the_arity_of o) . n) as SortSymbol of S;

          

           A7: ex ff be Function st ff = y & ( dom ff) = ( dom ( the_arity_of o)) & ( rng ff) c= ( Funcs (I,D)) by A1, FUNCT_2:def 2;

          then n in ( dom y) by A5, PRALG_2: 3;

          then (y . n) in ( rng y) by FUNCT_1:def 3;

          then

          consider g be Function such that

           A8: g = (y . n) and ( dom g) = I and ( rng g) c= D by A7, FUNCT_2:def 2;

          ((( commute y) . ii) . n) = (g . ii) & (g . ii) in (the Sorts of (A . ii) . s1) by A1, A6, A8, Th16, FUNCT_6: 56;

          hence ((( commute y) . ii) . n) in ((the Sorts of (A . ii) * ( the_arity_of o)) . n) by A5, FUNCT_1: 12;

        end;

        (( commute y) . ii) in ( rng ( commute y)) by A2, FUNCT_1:def 3;

        then ex h be Function st h = (( commute y) . ii) & ( dom h) = ( dom ( the_arity_of o)) & ( rng h) c= D by A2, FUNCT_2:def 2;

        then ( dom (( commute y) . ii)) = ( dom (the Sorts of (A . ii) * ( the_arity_of o))) by PRALG_2: 3;

        then (( commute y) . ii) in ( product (the Sorts of (A . ii) * ( the_arity_of o))) by A4, CARD_3: 9;

        then (( commute y) . ii) in ( Args (o,(A . ii))) by PRALG_2: 3;

        hence (( commute y) . i1) in (( doms (A ?. o)) . i1) by PRALG_2: 11;

      end;

      ( dom ( commute y)) = ( dom ( doms (A ?. o))) by A2, PRALG_2: 11;

      hence thesis by A3, CARD_3: 9;

    end;

    theorem :: PRALG_3:18

    

     Th18: for y be Element of ( Args (o,( product A))) st ( the_arity_of o) <> {} holds y in ( dom ( Commute ( Frege (A ?. o))))

    proof

      let y be Element of ( Args (o,( product A)));

      set D = ( union the set of all (the Sorts of (A . ii) . ss) where ii be Element of I, ss be Element of the carrier of S);

      assume

       A1: ( the_arity_of o) <> {} ;

      then ( commute y) in ( product ( doms (A ?. o))) by Th17;

      then

       A2: ( commute y) in ( dom ( Frege (A ?. o))) by PARTFUN1:def 2;

      y in ( Funcs (( dom ( the_arity_of o)),( Funcs (I,D)))) by Th14;

      then y = ( commute ( commute y)) by A1, FUNCT_6: 57;

      hence thesis by A2, PRALG_2:def 1;

    end;

    theorem :: PRALG_3:19

    

     Th19: for I be set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S, o be OperSymbol of S holds for x be Element of ( Args (o,( product A))) holds (( Den (o,( product A))) . x) in ( product ( Carrier (A,( the_result_sort_of o))))

    proof

      let I be set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S, o be OperSymbol of S;

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

      ( Result (o,( product A))) = (( SORTS A) . ( the_result_sort_of o)) by PRALG_2: 3

      .= ( product ( Carrier (A,( the_result_sort_of o)))) by PRALG_2:def 10;

      hence thesis;

    end;

    theorem :: PRALG_3:20

    

     Th20: for I, S, A, i holds for o be OperSymbol of S st ( the_arity_of o) <> {} holds for U1 be non-empty MSAlgebra over S holds for x be Element of ( Args (o,( product A))) holds (( commute x) . i) is Element of ( Args (o,(A . i)))

    proof

      let I, S, A, i;

      let o be OperSymbol of S such that

       A1: ( the_arity_of o) <> {} ;

      let U1 be non-empty MSAlgebra over S;

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

      i in I;

      then

       A2: i in ( dom ( doms (A ?. o))) by PRALG_2: 11;

      ( commute x) in ( product ( doms (A ?. o))) by A1, Th17;

      then (( commute x) . i) in (( doms (A ?. o)) . i) by A2, CARD_3: 9;

      hence thesis by PRALG_2: 11;

    end;

    theorem :: PRALG_3:21

    

     Th21: for I, S, A, i, o holds for x be Element of ( Args (o,( product A))) holds for n be set st n in ( dom ( the_arity_of o)) holds for f be Function st f = (x . n) holds ((( commute x) . i) . n) = (f . i)

    proof

      let I, S, A, i, o;

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

      let n be set such that

       A1: n in ( dom ( the_arity_of o));

      set C = ( union the set of all (the Sorts of (A . i9) . s9) where i9 be Element of I, s9 be Element of the carrier of S);

      

       A2: x in ( Funcs (( dom ( the_arity_of o)),( Funcs (I,C)))) by Th14;

      let g be Function;

      assume g = (x . n);

      hence thesis by A1, A2, FUNCT_6: 56;

    end;

    theorem :: PRALG_3:22

    

     Th22: for o be OperSymbol of S st ( the_arity_of o) <> {} holds for y be Element of ( Args (o,( product A))), i9 be Element of I holds for g be Function st g = (( Den (o,( product A))) . y) holds (g . i9) = (( Den (o,(A . i9))) . (( commute y) . i9))

    proof

      let o be OperSymbol of S such that

       A1: ( the_arity_of o) <> {} ;

      let y be Element of ( Args (o,( product A))), i9 be Element of I;

      

       A2: y in ( dom ( Commute ( Frege (A ?. o)))) by A1, Th18;

      

       A3: ( commute y) in ( product ( doms (A ?. o))) by A1, Th17;

      

       A4: ( Den (o,( product A))) = (( OPS A) . o) by MSUALG_1:def 6

      .= ( IFEQ (( the_arity_of o), {} ,( commute (A ?. o)),( Commute ( Frege (A ?. o))))) by PRALG_2:def 13

      .= ( Commute ( Frege (A ?. o))) by A1, FUNCOP_1:def 8;

      set C = ( union the set of all (the Sorts of (A . i9) . s9) where i9 be Element of I, s9 be Element of the carrier of S);

      y in ( Funcs (( dom ( the_arity_of o)),( Funcs (I,C)))) by Th14;

      then ( commute y) in ( Funcs (I,( Funcs (( dom ( the_arity_of o)),C)))) by A1, FUNCT_6: 55;

      then

       WW: ( dom ( commute y)) = I by FUNCT_2: 92;

      ( dom (A ?. o)) = I by PARTFUN1:def 2;

      

      then

       a5: ( dom ((A ?. o) .. ( commute y))) = (I /\ ( dom ( commute y))) by PRALG_1:def 19

      .= I by WW;

      let g be Function;

      assume g = (( Den (o,( product A))) . y);

      

      then g = (( Frege (A ?. o)) . ( commute y)) by A4, A2, PRALG_2:def 1

      .= ((A ?. o) .. ( commute y)) by A3, PRALG_2:def 2;

      

      then (g . i9) = (((A ?. o) . i9) . (( commute y) . i9)) by a5, PRALG_1:def 19

      .= (( Den (o,(A . i9))) . (( commute y) . i9)) by PRALG_2: 7;

      hence thesis;

    end;

    begin

    definition

      let I, S;

      let A be MSAlgebra-Family of I, S, i be Element of I;

      :: PRALG_3:def2

      func proj (A,i) -> ManySortedFunction of ( product A), (A . i) means

      : Def2: for s be Element of S holds (it . s) = ( proj (( Carrier (A,s)),i));

      existence

      proof

        deffunc G( Element of S) = ( proj (( Carrier (A,$1)),i));

        consider F be ManySortedSet of the carrier of S such that

         A1: for s be Element of S holds (F . s) = G(s) from PBOOLE:sch 5;

        F is ManySortedFunction of ( product A), (A . i)

        proof

          let s be object such that

           A2: s in the carrier of S;

          (F . s) is Function of (the Sorts of ( product A) . s), (the Sorts of (A . i) . s)

          proof

            reconsider s9 = s as Element of S by A2;

            (F . s) = ( proj (( Carrier (A,s9)),i)) by A1;

            then

            reconsider F9 = (F . s) as Function;

            

             A3: ( rng F9) c= (the Sorts of (A . i) . s)

            proof

              let y be object;

              

               A4: ( dom ( Carrier (A,s9))) = I & ex U0 be MSAlgebra over S st U0 = (A . i) & (( Carrier (A,s9)) . i) = (the Sorts of U0 . s9) by PARTFUN1:def 2, PRALG_2:def 9;

              assume y in ( rng F9);

              then y in ( rng ( proj (( Carrier (A,s9)),i))) by A1;

              then

              consider x1 be object such that

               A5: x1 in ( dom ( proj (( Carrier (A,s9)),i))) and

               A6: y = (( proj (( Carrier (A,s9)),i)) . x1) by FUNCT_1:def 3;

              

               A7: x1 in ( product ( Carrier (A,s9))) by A5;

              then

              reconsider x1 as Function;

              y = (x1 . i) by A5, A6, CARD_3:def 16;

              hence thesis by A7, A4, CARD_3: 9;

            end;

            ( dom F9) = ( dom ( proj (( Carrier (A,s9)),i))) by A1

            .= ( product ( Carrier (A,s9))) by CARD_3:def 16

            .= (the Sorts of ( product A) . s) by PRALG_2:def 10;

            hence thesis by A2, A3, FUNCT_2:def 1, RELSET_1: 4;

          end;

          hence thesis;

        end;

        then

        reconsider F9 = F as ManySortedFunction of ( product A), (A . i);

        take F9;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F,G be ManySortedFunction of ( product A), (A . i) such that

         A8: for s be Element of S holds (F . s) = ( proj (( Carrier (A,s)),i)) and

         A9: for s be Element of S holds (G . s) = ( proj (( Carrier (A,s)),i));

        now

          let s9 be object;

          assume s9 in the carrier of S;

          then

          reconsider s99 = s9 as Element of S;

          

          thus (F . s9) = ( proj (( Carrier (A,s99)),i)) by A8

          .= (G . s9) by A9;

        end;

        hence F = G;

      end;

    end

    theorem :: PRALG_3:23

    

     Th23: for x be Element of ( Args (o,( product A))) st ( the_arity_of o) <> {} holds for i be Element of I holds (( proj (A,i)) # x) = (( commute x) . i)

    proof

      let x be Element of ( Args (o,( product A))) such that

       A1: ( the_arity_of o) <> {} ;

      set C = ( union the set of all (the Sorts of (A . i9) . s9) where i9 be Element of I, s9 be Element of the carrier of S);

      let i be Element of I;

      

       A2: x in ( Funcs (( dom ( the_arity_of o)),( Funcs (I,C)))) by Th14;

      then

       A3: ( commute x) in ( Funcs (I,( Funcs (( dom ( the_arity_of o)),C)))) by A1, FUNCT_6: 55;

      then ( dom ( commute x)) = I by FUNCT_2: 92;

      then

       A4: (( commute x) . i) in ( rng ( commute x)) by FUNCT_1:def 3;

      

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

       A5:

      now

        

         A6: ( rng x) c= ( Funcs (I,C)) by A2, FUNCT_2: 92;

        let n be object such that

         A7: n in ( dom ( the_arity_of o));

        (x . n) in ( product ( Carrier (A,(( the_arity_of o) /. n)))) by A7, Th15;

        then

         A8: (x . n) in ( dom ( proj (( Carrier (A,(( the_arity_of o) /. n))),i))) by CARD_3:def 16;

        n in ( dom x) by A2, A7, FUNCT_2: 92;

        then (x . n) in ( rng x) by FUNCT_1:def 3;

        then

        consider g be Function such that

         A9: g = (x . n) and ( dom g) = I and ( rng g) c= C by A6, FUNCT_2:def 2;

        

        thus ((( proj (A,i)) # x) . n) = ((( proj (A,i)) . (( the_arity_of o) /. n)) . (x . n)) by A7, Th13

        .= (( proj (( Carrier (A,(( the_arity_of o) /. n))),i)) . (x . n)) by Def2

        .= (g . i) by A9, A8, CARD_3:def 16

        .= ((( commute x) . i) . n) by A2, A7, A9, FUNCT_6: 56;

      end;

      

       A10: x in ( product ( doms (( proj (A,i)) * ( the_arity_of o)))) by Th12;

      ( rng ( commute x)) c= ( Funcs (( dom ( the_arity_of o)),C)) by A3, FUNCT_2: 92;

      then

       A11: ( dom (( commute x) . i)) = ( dom ( the_arity_of o)) by A4, FUNCT_2: 92;

      ( dom ( proj (A,i))) = the carrier of S by PARTFUN1:def 2;

      then

       A12: ( rng ( the_arity_of o)) c= ( dom ( proj (A,i)));

      ( dom (( proj (A,i)) # x)) = ( dom (( Frege (( proj (A,i)) * ( the_arity_of o))) . x)) by MSUALG_3:def 5

      .= ( dom ((( proj (A,i)) * ( the_arity_of o)) .. x)) by A10, PRALG_2:def 2

      .= (( dom (( proj (A,i)) * ( the_arity_of o))) /\ ( dom x)) by PRALG_1:def 19

      .= (( dom ( the_arity_of o)) /\ ( dom x)) by A12, RELAT_1: 27;

      hence thesis by A11, A5, SS;

    end;

    theorem :: PRALG_3:24

    for i be Element of I holds for A be MSAlgebra-Family of I, S holds ( proj (A,i)) is_homomorphism (( product A),(A . i))

    proof

      let i be Element of I;

      let A be MSAlgebra-Family of I, S;

      thus ( proj (A,i)) is_homomorphism (( product A),(A . i))

      proof

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

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

        set F = ( proj (A,i)), s = ( the_result_sort_of o);

        o in the carrier' of S;

        then

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

        

         A2: ( Result (o,( product A))) = ((the Sorts of ( product A) * the ResultSort of S) . o) by MSUALG_1:def 5

        .= (the Sorts of ( product A) . (the ResultSort of S . o)) by A1, FUNCT_1: 13

        .= (( SORTS A) . s) by MSUALG_1:def 2

        .= ( product ( Carrier (A,s))) by PRALG_2:def 10;

        thus ((F . s) . (( Den (o,( product A))) . x)) = (( Den (o,(A . i))) . (F # x))

        proof

          per cases ;

            suppose

             A3: ( the_arity_of o) = {} ;

            then ( const (o,( product A))) in ( product ( Carrier (A,s))) by A2, Th5;

            then

             A4: ( const (o,( product A))) in ( dom ( proj (( Carrier (A,s)),i))) by CARD_3:def 16;

            

             A5: ( Args (o,( product A))) = { {} } by A3, PRALG_2: 4;

            then

             A6: x = {} by TARSKI:def 1;

            ((F . s) . (( Den (o,( product A))) . x)) = ((F . s) . ( const (o,( product A)))) by A5, TARSKI:def 1

            .= (( proj (( Carrier (A,s)),i)) . ( const (o,( product A)))) by Def2

            .= (( const (o,( product A))) . i) by A4, CARD_3:def 16

            .= ( const (o,(A . i))) by A3, Th9

            .= (( Den (o,(A . i))) . (F # x)) by A3, A6, Th11;

            hence thesis;

          end;

            suppose

             A7: ( the_arity_of o) <> {} ;

            reconsider D = (( Den (o,( product A))) . x) as Function by A2;

            (( Den (o,( product A))) . x) in ( product ( Carrier (A,s))) by A2;

            then

             A8: (( Den (o,( product A))) . x) in ( dom ( proj (( Carrier (A,s)),i))) by CARD_3:def 16;

            ((F . s) . (( Den (o,( product A))) . x)) = (( proj (( Carrier (A,s)),i)) . (( Den (o,( product A))) . x)) by Def2

            .= (D . i) by A8, CARD_3:def 16

            .= (( Den (o,(A . i))) . (( commute x) . i)) by A7, Th22

            .= (( Den (o,(A . i))) . (( proj (A,i)) # x)) by A7, Th23;

            hence thesis;

          end;

        end;

      end;

    end;

    theorem :: PRALG_3:25

    

     Th25: for U1 be non-empty MSAlgebra over S holds for F be ManySortedFunction of I st (for i be Element of I holds ex F1 be ManySortedFunction of U1, (A . i) st F1 = (F . i) & F1 is_homomorphism (U1,(A . i))) holds F in ( Funcs (I,( Funcs (the carrier of S, the set of all ((F . i9) . s1) where s1 be SortSymbol of S, i9 be Element of I)))) & ((( commute F) . s) . i) = ((F . i) . s)

    proof

      let U1 be non-empty MSAlgebra over S;

      let F be ManySortedFunction of I such that

       A1: for i be Element of I holds ex F1 be ManySortedFunction of U1, (A . i) st F1 = (F . i) & F1 is_homomorphism (U1,(A . i));

      set FS = the set of all ((F . i9) . s1) where s1 be SortSymbol of S, i9 be Element of I;

      set CA = the carrier of S;

      

       A2: ( rng F) c= ( Funcs (CA,FS))

      proof

        let x be object;

        assume x in ( rng F);

        then

        consider i9 be object such that

         A3: i9 in ( dom F) and

         A4: (F . i9) = x by FUNCT_1:def 3;

        reconsider i1 = i9 as Element of I by A3;

        consider F9 be ManySortedFunction of U1, (A . i1) such that

         A5: F9 = (F . i1) and F9 is_homomorphism (U1,(A . i1)) by A1;

        

         A6: ( rng F9) c= FS

        proof

          let x9 be object;

          assume x9 in ( rng F9);

          then

          consider s9 be object such that

           A7: s9 in ( dom F9) and

           A8: (F9 . s9) = x9 by FUNCT_1:def 3;

          s9 is SortSymbol of S by A7;

          hence thesis by A5, A8;

        end;

        ( dom F9) = CA by PARTFUN1:def 2;

        hence thesis by A4, A5, A6, FUNCT_2:def 2;

      end;

      

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

      hence F in ( Funcs (I,( Funcs (CA,FS)))) by A2, FUNCT_2:def 2;

      F in ( Funcs (I,( Funcs (CA,FS)))) by A9, A2, FUNCT_2:def 2;

      hence thesis by FUNCT_6: 56;

    end;

    theorem :: PRALG_3:26

    

     Th26: for U1 be non-empty MSAlgebra over S holds for F be ManySortedFunction of I st (for i be Element of I holds ex F1 be ManySortedFunction of U1, (A . i) st F1 = (F . i) & F1 is_homomorphism (U1,(A . i))) holds (( commute F) . s) in ( Funcs (I,( Funcs ((the Sorts of U1 . s),( union the set of all (the Sorts of (A . i9) . s1) where i9 be Element of I, s1 be SortSymbol of S)))))

    proof

      let U1 be non-empty MSAlgebra over S;

      let F be ManySortedFunction of I such that

       A1: for i be Element of I holds ex F1 be ManySortedFunction of U1, (A . i) st F1 = (F . i) & F1 is_homomorphism (U1,(A . i));

      set SU = the Sorts of U1, CA = the carrier of S, SA = ( union the set of all (the Sorts of (A . i9) . s1) where i9 be Element of I, s1 be SortSymbol of S);

      set SA9 = the set of all (the Sorts of (A . i9) . s1) where i9 be Element of I, s1 be SortSymbol of S;

      set FS = the set of all ((F . i9) . s1) where s1 be SortSymbol of S, i9 be Element of I;

      F in ( Funcs (I,( Funcs (CA,FS)))) by A1, Th25;

      then ( commute F) in ( Funcs (CA,( Funcs (I,FS)))) by FUNCT_6: 55;

      then

      consider F9 be Function such that

       A2: F9 = ( commute F) & ( dom F9) = CA and

       A3: ( rng F9) c= ( Funcs (I,FS)) by FUNCT_2:def 2;

      (( commute F) . s) in ( rng F9) by A2, FUNCT_1:def 3;

      then

       A4: ex F2 be Function st F2 = (( commute F) . s) & ( dom F2) = I & ( rng F2) c= FS by A3, FUNCT_2:def 2;

      ( rng (( commute F) . s)) c= ( Funcs ((SU . s),SA))

      proof

        let x9 be object;

        assume x9 in ( rng (( commute F) . s));

        then

        consider i9 be object such that

         A5: i9 in ( dom (( commute F) . s)) and

         A6: x9 = ((( commute F) . s) . i9) by FUNCT_1:def 3;

        reconsider i1 = i9 as Element of I by A4, A5;

        consider F9 be ManySortedFunction of U1, (A . i1) such that

         A7: F9 = (F . i1) and F9 is_homomorphism (U1,(A . i1)) by A1;

        (the Sorts of (A . i1) . s) c= SA

        proof

          

           A8: (the Sorts of (A . i1) . s) in SA9;

          let y be object;

          assume y in (the Sorts of (A . i1) . s);

          hence thesis by A8, TARSKI:def 4;

        end;

        then

         A9: ( dom (F9 . s)) = (SU . s) & ( rng (F9 . s)) c= SA by FUNCT_2:def 1;

        x9 = (F9 . s) by A1, A6, A7, Th25;

        hence thesis by A9, FUNCT_2:def 2;

      end;

      hence thesis by A4, FUNCT_2:def 2;

    end;

    theorem :: PRALG_3:27

    

     Th27: for U1 be non-empty MSAlgebra over S holds for F be ManySortedFunction of I st (for i be Element of I holds ex F1 be ManySortedFunction of U1, (A . i) st F1 = (F . i) & F1 is_homomorphism (U1,(A . i))) holds for F9 be ManySortedFunction of U1, (A . i) st F9 = (F . i) holds for x be set st x in (the Sorts of U1 . s) holds for f be Function st f = (( commute (( commute F) . s)) . x) holds (f . i) = ((F9 . s) . x)

    proof

      let U1 be non-empty MSAlgebra over S;

      set SU = the Sorts of U1, SA = ( union the set of all (the Sorts of (A . i9) . s1) where i9 be Element of I, s1 be SortSymbol of S);

      let F be ManySortedFunction of I such that

       A1: for i be Element of I holds ex F1 be ManySortedFunction of U1, (A . i) st F1 = (F . i) & F1 is_homomorphism (U1,(A . i));

      

       A2: (( commute F) . s) in ( Funcs (I,( Funcs ((SU . s),SA)))) by A1, Th26;

      then ( dom (( commute F) . s)) = I by FUNCT_2: 92;

      then

       A3: ((( commute F) . s) . i) in ( rng (( commute F) . s)) by FUNCT_1:def 3;

      reconsider f9 = (( commute F) . s) as Function;

      ( rng (( commute F) . s)) c= ( Funcs ((SU . s),SA)) by A2, FUNCT_2: 92;

      then

      consider g be Function such that

       A4: g = (f9 . i) and ( dom g) = (SU . s) and ( rng g) c= SA by A3, FUNCT_2:def 2;

      let F9 be ManySortedFunction of U1, (A . i) such that

       A5: F9 = (F . i);

      let x1 be set such that

       A6: x1 in (the Sorts of U1 . s);

      let f be Function such that

       A7: f = (( commute (( commute F) . s)) . x1);

      g = (F9 . s) by A1, A5, A4, Th25;

      hence thesis by A6, A7, A2, A4, FUNCT_6: 56;

    end;

    theorem :: PRALG_3:28

    

     Th28: for U1 be non-empty MSAlgebra over S holds for F be ManySortedFunction of I st (for i be Element of I holds ex F1 be ManySortedFunction of U1, (A . i) st F1 = (F . i) & F1 is_homomorphism (U1,(A . i))) holds for x be set st x in (the Sorts of U1 . s) holds (( commute (( commute F) . s)) . x) in ( product ( Carrier (A,s)))

    proof

      let U1 be non-empty MSAlgebra over S;

      set SU = the Sorts of U1, SA = ( union the set of all (the Sorts of (A . i9) . s1) where i9 be Element of I, s1 be SortSymbol of S);

      let F be ManySortedFunction of I such that

       A1: for i be Element of I holds ex F1 be ManySortedFunction of U1, (A . i) st F1 = (F . i) & F1 is_homomorphism (U1,(A . i));

      (( commute F) . s) in ( Funcs (I,( Funcs ((SU . s),SA)))) by A1, Th26;

      then ( commute (( commute F) . s)) in ( Funcs ((SU . s),( Funcs (I,SA)))) by FUNCT_6: 55;

      then

      consider f9 be Function such that

       A2: f9 = ( commute (( commute F) . s)) and

       A3: ( dom f9) = (SU . s) and

       A4: ( rng f9) c= ( Funcs (I,SA)) by FUNCT_2:def 2;

      let x be set such that

       A5: x in (the Sorts of U1 . s);

      (f9 . x) in ( rng f9) by A5, A3, FUNCT_1:def 3;

      then

      consider f be Function such that

       A6: f = (( commute (( commute F) . s)) . x) and

       A7: ( dom f) = I and ( rng f) c= SA by A2, A4, FUNCT_2:def 2;

       A8:

      now

        let i1 be object;

        assume i1 in ( dom ( Carrier (A,s)));

        then

        reconsider i9 = i1 as Element of I;

        consider F1 be ManySortedFunction of U1, (A . i9) such that

         A9: F1 = (F . i9) and F1 is_homomorphism (U1,(A . i9)) by A1;

        x in ( dom (F1 . s)) by A5, FUNCT_2:def 1;

        then

         A10: (ex U0 be MSAlgebra over S st U0 = (A . i9) & (( Carrier (A,s)) . i9) = (the Sorts of U0 . s)) & ((F1 . s) . x) in ( rng (F1 . s)) by FUNCT_1:def 3, PRALG_2:def 9;

        (f . i9) = ((F1 . s) . x) by A1, A5, A6, A9, Th27;

        hence ((( commute (( commute F) . s)) . x) . i1) in (( Carrier (A,s)) . i1) by A6, A10;

      end;

      ( dom (( commute (( commute F) . s)) . x)) = ( dom ( Carrier (A,s))) by A6, A7, PARTFUN1:def 2;

      hence thesis by A8, CARD_3: 9;

    end;

    theorem :: PRALG_3:29

    for U1 be non-empty MSAlgebra over S holds for F be ManySortedFunction of I st (for i be Element of I holds ex F1 be ManySortedFunction of U1, (A . i) st F1 = (F . i) & F1 is_homomorphism (U1,(A . i))) holds ex H be ManySortedFunction of U1, ( product A) st H is_homomorphism (U1,( product A)) & for i be Element of I holds (( proj (A,i)) ** H) = (F . i)

    proof

      let U1 be non-empty MSAlgebra over S;

      let F be ManySortedFunction of I such that

       A1: for i be Element of I holds ex F1 be ManySortedFunction of U1, (A . i) st F1 = (F . i) & F1 is_homomorphism (U1,(A . i));

      set SU = the Sorts of U1, CA = the carrier of S, SA = ( union the set of all (the Sorts of (A . i9) . s1) where i9 be Element of I, s1 be SortSymbol of S);

      deffunc G( Element of S) = ( commute (( commute F) . $1));

      consider H be ManySortedSet of the carrier of S such that

       A2: for s9 be Element of the carrier of S holds (H . s9) = G(s9) from PBOOLE:sch 5;

      now

        let s9 be object;

        assume

         A3: s9 in the carrier of S;

        then

        reconsider s99 = s9 as SortSymbol of S;

        (( commute F) . s9) in ( Funcs (I,( Funcs ((SU . s9),SA)))) by A1, A3, Th26;

        then ( commute (( commute F) . s9)) in ( Funcs ((SU . s9),( Funcs (I,SA)))) by A3, FUNCT_6: 55;

        then (H . s9) in ( Funcs ((SU . s9),( Funcs (I,SA)))) by A2, A3;

        then

        consider Hs be Function such that

         A4: Hs = (H . s9) and

         A5: ( dom Hs) = (SU . s9) and

         A6: ( rng Hs) c= ( Funcs (I,SA)) by FUNCT_2:def 2;

        ( rng Hs) c= (the Sorts of ( product A) . s9)

        proof

          let x be object;

          assume

           A7: x in ( rng Hs);

          then

          consider f be Function such that

           A8: f = x and

           A9: ( dom f) = I and ( rng f) c= SA by A6, FUNCT_2:def 2;

          consider x1 be object such that

           A10: x1 in ( dom Hs) and

           A11: (Hs . x1) = f by A7, A8, FUNCT_1:def 3;

           A12:

          now

            let i9 be object;

            assume i9 in ( dom ( Carrier (A,s99)));

            then

            reconsider i99 = i9 as Element of I;

            consider F9 be ManySortedFunction of U1, (A . i99) such that

             A13: F9 = (F . i99) and F9 is_homomorphism (U1,(A . i99)) by A1;

            (H . s99) = ( commute (( commute F) . s99)) by A2;

            then

             A14: (f . i99) = ((F9 . s99) . x1) by A1, A4, A5, A10, A11, A13, Th27;

            ( dom (F9 . s99)) = ( dom Hs) by A5, FUNCT_2:def 1;

            then

             A15: ((F9 . s9) . x1) in ( rng (F9 . s9)) by A10, FUNCT_1:def 3;

            (ex U0 be MSAlgebra over S st U0 = (A . i99) & (( Carrier (A,s99)) . i99) = (the Sorts of U0 . s99)) & ( rng (F9 . s99)) c= (the Sorts of (A . i99) . s99) by PRALG_2:def 9;

            hence (f . i9) in (( Carrier (A,s99)) . i9) by A14, A15;

          end;

          ( dom ( Carrier (A,s99))) = ( dom f) by A9, PARTFUN1:def 2;

          then f in ( product ( Carrier (A,s99))) by A12, CARD_3: 9;

          hence thesis by A8, PRALG_2:def 10;

        end;

        hence (H . s9) is Function of (the Sorts of U1 . s9), (the Sorts of ( product A) . s9) by A3, A4, A5, FUNCT_2:def 1, RELSET_1: 4;

      end;

      then

      reconsider H as ManySortedFunction of U1, ( product A) by PBOOLE:def 15;

      

       A16: H is_homomorphism (U1,( product A))

      proof

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

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

        set s9 = ( the_result_sort_of o);

        

         A17: ( Result (o,U1)) = (the Sorts of U1 . ( the_result_sort_of o)) by PRALG_2: 3;

        then

         A18: (( Den (o,U1)) . x) in (SU . s9);

        thus ((H . ( the_result_sort_of o)) . (( Den (o,U1)) . x)) = (( Den (o,( product A))) . (H # x))

        proof

          per cases ;

            suppose

             A19: ( the_arity_of o) = {} ;

            set f = (( commute (( commute F) . s9)) . ( const (o,U1)));

            ( Args (o,U1)) = { {} } by A19, PRALG_2: 4;

            then

             A20: x = {} by TARSKI:def 1;

             A21:

            now

              let i9 be object;

              assume i9 in I;

              then

              reconsider ii = i9 as Element of I;

              consider F1 be ManySortedFunction of U1, (A . ii) such that

               A22: F1 = (F . ii) and

               A23: F1 is_homomorphism (U1,(A . ii)) by A1;

              

               A24: (F1 # x) = {} by A19, A20, Th11;

              

              thus (f . i9) = ((F1 . ( the_result_sort_of o)) . (( Den (o,U1)) . x)) by A1, A17, A20, A22, Th27

              .= ( const (o,(A . ii))) by A23, A24

              .= (( const (o,( product A))) . i9) by A19, Th9;

            end;

            ( const (o,( product A))) in ( Funcs (I,( union the set of all ( Result (o,(A . i1))) where i1 be Element of I))) by A19, Th8;

            then

             A25: ex Co be Function st Co = ( const (o,( product A))) & ( dom Co) = I & ( rng Co) c= ( union the set of all ( Result (o,(A . i1))) where i1 be Element of I) by FUNCT_2:def 2;

            f in ( product ( Carrier (A,s9))) by A1, A18, A20, Th28;

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

            then

             A26: f = ( const (o,( product A))) by A25, A21;

            (H # x) = {} by A19, A20, Th11;

            hence thesis by A2, A20, A26;

          end;

            suppose

             A27: ( the_arity_of o) <> {} ;

            

             A28: ( Den (o,( product A))) = (( OPS A) . o) by MSUALG_1:def 6

            .= ( IFEQ (( the_arity_of o), {} ,( commute (A ?. o)),( Commute ( Frege (A ?. o))))) by PRALG_2:def 13

            .= ( Commute ( Frege (A ?. o))) by A27, FUNCOP_1:def 8;

             A29:

            now

              let y be Element of ( Args (o,( product A)));

              ( commute y) in ( product ( doms (A ?. o))) by A27, Th17;

              then

               A30: ( commute y) in ( dom ( Frege (A ?. o))) by PARTFUN1:def 2;

              y in ( dom ( Commute ( Frege (A ?. o)))) by A27, Th18;

              then (( Den (o,( product A))) . y) = (( Frege (A ?. o)) . ( commute y)) by A28, PRALG_2:def 1;

              hence (( Den (o,( product A))) . y) in ( rng ( Frege (A ?. o))) by A30, FUNCT_1:def 3;

            end;

            then

            reconsider f1 = (( Den (o,( product A))) . (H # x)) as Function by PRALG_2: 8;

            f1 in ( rng ( Frege (A ?. o))) by A29;

            then

             A31: ( dom f1) = I by PRALG_2: 9;

            set D = ( union the set of all (the Sorts of (A . i9) . ss) where i9 be Element of I, ss be Element of the carrier of S);

            set f = (( commute (( commute F) . s9)) . (( Den (o,U1)) . x));

            

             A32: (H # x) in ( Funcs (( dom ( the_arity_of o)),( Funcs (I,D)))) by Th14;

             A33:

            now

              let i9 be object;

              assume i9 in I;

              then

              reconsider ii = i9 as Element of I;

              consider F1 be ManySortedFunction of U1, (A . ii) such that

               A34: F1 = (F . ii) and

               A35: F1 is_homomorphism (U1,(A . ii)) by A1;

              

               A36: ((F1 . ( the_result_sort_of o)) . (( Den (o,U1)) . x)) = (( Den (o,(A . ii))) . (F1 # x)) by A35;

              x in ( Args (o,U1));

              then

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

              then

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

              

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

               A37:

              now

                let n be object;

                assume

                 A38: n in ( dom ( the_arity_of o));

                then (( the_arity_of o) . n) in ( rng ( the_arity_of o)) by FUNCT_1:def 3;

                then

                reconsider s1 = (( the_arity_of o) . n) as Element of the carrier of S;

                

                 A39: ((F1 # x) . n) = ((F1 . (( the_arity_of o) /. n)) . (x . n)) by A38, Th13

                .= ((F1 . s1) . (x . n)) by A38, PARTFUN1:def 6;

                (x . n) in ((the Sorts of U1 * ( the_arity_of o)) . n) by A38, A40, A41, A42, CARD_3: 9;

                then

                 A43: (x . n) in (SU . s1) by A38, A42, A41, FUNCT_1: 12;

                

                 A44: ((H # x) . n) = ((H . (( the_arity_of o) /. n)) . (x . n)) by A38, Th13

                .= ((H . s1) . (x . n)) by A38, PARTFUN1:def 6

                .= (( commute (( commute F) . s1)) . (x . n)) by A2;

                then

                reconsider g = ((H # x) . n) as Function;

                

                thus ((( commute (H # x)) . ii) . n) = (g . ii) by A32, A38, FUNCT_6: 56

                .= ((F1 # x) . n) by A1, A34, A43, A39, A44, Th27;

              end;

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

              then

               A45: ( rng ( the_arity_of o)) c= ( dom F1);

              ( commute (H # x)) in ( Funcs (I,( Funcs (( dom ( the_arity_of o)),D)))) by A27, A32, FUNCT_6: 55;

              then

              consider ff be Function such that

               A46: ff = ( commute (H # x)) and

               A47: ( dom ff) = I and

               A48: ( rng ff) c= ( Funcs (( dom ( the_arity_of o)),D)) by FUNCT_2:def 2;

              (ff . ii) in ( rng ff) by A47, FUNCT_1:def 3;

              then

               A49: ex gg be Function st gg = (( commute (H # x)) . ii) & ( dom gg) = ( dom ( the_arity_of o)) & ( rng gg) c= D by A46, A48, FUNCT_2:def 2;

              

               A50: x in ( product ( doms (F1 * ( the_arity_of o)))) by Th12;

              ( dom (F1 # x)) = ( dom (( Frege (F1 * ( the_arity_of o))) . x)) by MSUALG_3:def 5

              .= ( dom ((F1 * ( the_arity_of o)) .. x)) by A50, PRALG_2:def 2

              .= (( dom (F1 * ( the_arity_of o))) /\ ( dom x)) by PRALG_1:def 19

              .= (( dom ( the_arity_of o)) /\ ( dom x)) by A45, RELAT_1: 27

              .= ( dom ( the_arity_of o)) by A42;

              then (F1 # x) = (( commute (H # x)) . ii) by A49, A37;

              

              then (f . i9) = (( Den (o,(A . ii))) . (( commute (H # x)) . ii)) by A1, A17, A34, A36, Th27

              .= (f1 . i9) by A27, Th22;

              hence (f . i9) = (f1 . i9);

            end;

            (( commute (( commute F) . s9)) . (( Den (o,U1)) . x)) in ( product ( Carrier (A,s9))) by A1, A17, Th28;

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

            then (( commute (( commute F) . s9)) . (( Den (o,U1)) . x)) = f1 by A31, A33;

            hence thesis by A2;

          end;

        end;

      end;

      take H;

      for i be Element of I holds (( proj (A,i)) ** H) = (F . i)

      proof

        let i be Element of I;

        consider F1 be ManySortedFunction of U1, (A . i) such that

         A51: F1 = (F . i) and F1 is_homomorphism (U1,(A . i)) by A1;

        

         A52: ( dom (( proj (A,i)) ** H)) = (( dom ( proj (A,i))) /\ ( dom H)) by PBOOLE:def 19

        .= (CA /\ ( dom H)) by PARTFUN1:def 2

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

        .= CA;

         A53:

        now

          let s9 be object;

          assume s9 in CA;

          then

          reconsider s1 = s9 as SortSymbol of S;

          

           A54: ((( proj (A,i)) ** H) . s9) = ((( proj (A,i)) . s1) * (H . s1)) by A52, PBOOLE:def 19

          .= (( proj (( Carrier (A,s1)),i)) * (H . s1)) by Def2

          .= (( proj (( Carrier (A,s1)),i)) * ( commute (( commute F) . s1))) by A2;

          (( commute F) . s1) in ( Funcs (I,( Funcs ((SU . s1),SA)))) by A1, Th26;

          then ( commute (( commute F) . s1)) in ( Funcs ((SU . s1),( Funcs (I,SA)))) by FUNCT_6: 55;

          then

          consider f9 be Function such that

           A55: f9 = ( commute (( commute F) . s1)) and

           A56: ( dom f9) = (SU . s1) and ( rng f9) c= ( Funcs (I,SA)) by FUNCT_2:def 2;

          ( rng f9) c= ( dom ( proj (( Carrier (A,s1)),i)))

          proof

            let y be object;

            assume y in ( rng f9);

            then

            consider x9 be object such that

             A57: x9 in ( dom f9) and

             A58: (f9 . x9) = y by FUNCT_1:def 3;

            (( commute (( commute F) . s1)) . x9) in ( product ( Carrier (A,s1))) by A1, A56, A57, Th28;

            hence thesis by A55, A58, CARD_3:def 16;

          end;

          then

           A59: ( dom ((( proj (A,i)) ** H) . s9)) = (SU . s9) by A55, A56, A54, RELAT_1: 27;

           A60:

          now

            let x be object;

            assume

             A61: x in (SU . s9);

            then (( commute (( commute F) . s1)) . x) in ( product ( Carrier (A,s1))) by A1, Th28;

            then

             A62: (( commute (( commute F) . s1)) . x) in ( dom ( proj (( Carrier (A,s1)),i))) by CARD_3:def 16;

            

            thus (((( proj (A,i)) ** H) . s9) . x) = (( proj (( Carrier (A,s1)),i)) . (( commute (( commute F) . s1)) . x)) by A54, A59, A61, FUNCT_1: 12

            .= ((( commute (( commute F) . s1)) . x) . i) by A62, CARD_3:def 16

            .= ((F1 . s9) . x) by A1, A51, A61, Th27;

          end;

          ( dom (F1 . s9)) = ( dom (F1 . s1))

          .= (SU . s9) by FUNCT_2:def 1;

          hence ((( proj (A,i)) ** H) . s9) = (F1 . s9) by A59, A60;

        end;

        ( dom F1) = CA by PARTFUN1:def 2;

        hence thesis by A51, A52, A53;

      end;

      hence thesis by A16;

    end;

    begin

    definition

      let I, J, S;

      :: PRALG_3:def3

      mode MSAlgebra-Class of S,J -> ManySortedSet of I means

      : Def3: for i be set st i in I holds (it . i) is MSAlgebra-Family of (J . i), S;

      existence

      proof

        defpred P[ object, object] means $2 is MSAlgebra-Family of (J . $1), S;

        

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

        proof

          let i be object such that i in I;

          set F = the MSAlgebra-Family of (J . i), S;

          take F;

          thus thesis;

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

        take C;

        thus thesis by A2;

      end;

    end

    definition

      let I, S, A, EqR;

      :: PRALG_3:def4

      func A / EqR -> MSAlgebra-Class of S, ( id ( Class EqR)) means

      : Def4: for c st c in ( Class EqR) holds (it . c) = (A | c);

      existence

      proof

        thus ex X be MSAlgebra-Class of S, ( id ( Class EqR)) st for c st c in ( Class EqR) holds (X . c) = (A | c)

        proof

          deffunc F( set) = (A | $1);

          consider X be ManySortedSet of ( Class EqR) such that

           A1: for c st c in ( Class EqR) holds (X . c) = F(c) from PBOOLE:sch 7;

          X is MSAlgebra-Class of S, ( id ( Class EqR))

          proof

            let c be set;

            assume

             A2: c in ( Class EqR);

            

             A3: ( dom (A | c)) = (( dom A) /\ c) by RELAT_1: 61

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

            .= c by A2, XBOOLE_1: 28

            .= (( id ( Class EqR)) . c) by A2, FUNCT_1: 18;

            then

            reconsider ac = (A | c) as ManySortedSet of (( id ( Class EqR)) . c) by PARTFUN1:def 2, RELAT_1:def 18;

            ac is MSAlgebra-Family of (( id ( Class EqR)) . c), S

            proof

              let i be object;

              assume

               A4: i in (( id ( Class EqR)) . c);

              ( dom ac) = c by A2, A3, FUNCT_1: 18;

              then

              reconsider i9 = i as Element of I by A2, A3, A4;

              (A . i9) is non-empty MSAlgebra over S;

              hence thesis by A3, A4, FUNCT_1: 47;

            end;

            hence thesis by A1, A2;

          end;

          then

          reconsider X as MSAlgebra-Class of S, ( id ( Class EqR));

          take X;

          thus thesis by A1;

        end;

      end;

      uniqueness

      proof

        for X,Y be MSAlgebra-Class of S, ( id ( Class EqR)) st (for c st c in ( Class EqR) holds (X . c) = (A | c)) & for c st c in ( Class EqR) holds (Y . c) = (A | c) holds X = Y

        proof

          let X,Y be MSAlgebra-Class of S, ( id ( Class EqR)) such that

           A5: for c st c in ( Class EqR) holds (X . c) = (A | c) and

           A6: for c st c in ( Class EqR) holds (Y . c) = (A | c);

          now

            let c be object;

            assume

             A7: c in ( Class EqR);

            reconsider cc = c as set by TARSKI: 1;

            

            thus (X . c) = (A | cc) by A5, A7

            .= (Y . c) by A6, A7;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let I, S;

      let J be non-empty ManySortedSet of I;

      let C be MSAlgebra-Class of S, J;

      :: PRALG_3:def5

      func product C -> MSAlgebra-Family of I, S means

      : Def5: for i st i in I holds ex Ji be non empty set, Cs be MSAlgebra-Family of Ji, S st Ji = (J . i) & Cs = (C . i) & (it . i) = ( product Cs);

      existence

      proof

        thus ex PC be MSAlgebra-Family of I, S st for i st i in I holds ex Ji be non empty set, Cs be MSAlgebra-Family of Ji, S st Ji = (J . i) & Cs = (C . i) & (PC . i) = ( product Cs)

        proof

          defpred P[ object, object] means ex Ji be non empty set, Cs be MSAlgebra-Family of Ji, S st Ji = (J . $1) & Cs = (C . $1) & $2 = ( product Cs);

           A1:

          now

            let i be object;

            assume

             A2: i in I;

            then

            reconsider Ji = (J . i) as non empty set;

            reconsider Cs = (C . i) as MSAlgebra-Family of Ji, S by A2, Def3;

            ex a be object st a = ( product Cs);

            then

            consider j be object such that

             A3: ex Ji be non empty set, Cs be MSAlgebra-Family of Ji, S st Ji = (J . i) & Cs = (C . i) & j = ( product Cs);

            reconsider j as object;

            take j;

            thus P[i, j] by A3;

          end;

          consider PC be ManySortedSet of I such that

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

          now

            let i be object;

            assume i in I;

            then ex Ji be non empty set, Cs be MSAlgebra-Family of Ji, S st Ji = (J . i) & Cs = (C . i) & (PC . i) = ( product Cs) by A4;

            hence (PC . i) is non-empty MSAlgebra over S;

          end;

          then

          reconsider PC as MSAlgebra-Family of I, S by PRALG_2:def 5;

          take PC;

          thus thesis by A4;

        end;

      end;

      uniqueness

      proof

        for PC1,PC2 be MSAlgebra-Family of I, S st (for i st i in I holds ex Ji be non empty set, Cs be MSAlgebra-Family of Ji, S st Ji = (J . i) & Cs = (C . i) & (PC1 . i) = ( product Cs)) & for i st i in I holds ex Ji be non empty set, Cs be MSAlgebra-Family of Ji, S st Ji = (J . i) & Cs = (C . i) & (PC2 . i) = ( product Cs) holds PC1 = PC2

        proof

          let PC1,PC2 be MSAlgebra-Family of I, S such that

           A5: (for i st i in I holds ex Ji be non empty set, Cs be MSAlgebra-Family of Ji, S st Ji = (J . i) & Cs = (C . i) & (PC1 . i) = ( product Cs)) & for i st i in I holds ex Ji be non empty set, Cs be MSAlgebra-Family of Ji, S st Ji = (J . i) & Cs = (C . i) & (PC2 . i) = ( product Cs);

          now

            let i1 be object;

            assume i1 in I;

            then

            reconsider i9 = i1 as Element of I;

            (ex Ji1 be non empty set, Cs1 be MSAlgebra-Family of Ji1, S st Ji1 = (J . i9) & Cs1 = (C . i9) & (PC1 . i9) = ( product Cs1)) & ex Ji2 be non empty set, Cs2 be MSAlgebra-Family of Ji2, S st Ji2 = (J . i9) & Cs2 = (C . i9) & (PC2 . i9) = ( product Cs2) by A5;

            hence (PC1 . i1) = (PC2 . i1);

          end;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: PRALG_3:30

    for A be MSAlgebra-Family of I, S, EqR be Equivalence_Relation of I holds (( product A),( product ( product (A / EqR)))) are_isomorphic

    proof

      let A be MSAlgebra-Family of I, S, EqR be Equivalence_Relation of I;

      set U1 = ( product A), U2 = ( product ( product (A / EqR)));

      set U19 = the Sorts of U1, U29 = the Sorts of U2;

      defpred P[ object, object, object] means for f1,g1 be Function st f1 = $2 & g1 = $1 holds for e be Element of ( Class EqR) holds (g1 . e) = (f1 | e);

      

       A1: for s be object st s in the carrier of S holds for x be object st x in (U19 . s) holds ex y be object st y in (U29 . s) & P[y, x, s]

      proof

        let s be object;

        assume s in the carrier of S;

        then

        reconsider s9 = s as SortSymbol of S;

        

         A2: (U19 . s9) = ( product ( Carrier (A,s9))) by PRALG_2:def 10;

        let x be object such that

         A3: x in (U19 . s);

        reconsider x as Function by A3, A2;

        deffunc F( set) = (x | $1);

        consider y be ManySortedSet of ( Class EqR) such that

         A4: for c st c in ( Class EqR) holds (y . c) = F(c) from PBOOLE:sch 7;

        

         A5: ( dom ( Carrier (( product (A / EqR)),s9))) = ( Class EqR) by PARTFUN1:def 2;

        

         A6: for a be object st a in ( dom ( Carrier (( product (A / EqR)),s9))) holds (y . a) in (( Carrier (( product (A / EqR)),s9)) . a)

        proof

          set A9 = ( product (A / EqR));

          let a be object such that

           A7: a in ( dom ( Carrier (( product (A / EqR)),s9)));

          reconsider a as set by TARSKI: 1;

          

           A8: ((A / EqR) . a) = (A | a) by A7, Def4;

          reconsider a as non empty Subset of I by A5, A7;

          

           A9: ex U0 be MSAlgebra over S st U0 = (A9 . a) & (( Carrier (A9,s9)) . a) = (the Sorts of U0 . s9) by A7, PRALG_2:def 9;

          

           A10: ( dom (A | a)) = (( dom A) /\ a) by RELAT_1: 61

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

          .= a by XBOOLE_1: 28;

          then

          reconsider Aa1 = (A | a) as ManySortedSet of a by PARTFUN1:def 2;

          for i be object st i in a holds (Aa1 . i) is non-empty MSAlgebra over S

          proof

            let i be object;

            assume

             A11: i in a;

            then (A . i) is non-empty MSAlgebra over S by PRALG_2:def 5;

            hence thesis by A10, A11, FUNCT_1: 47;

          end;

          then

          reconsider Aa = Aa1 as MSAlgebra-Family of a, S by PRALG_2:def 5;

          (x | a) in ( product (( Carrier (A,s9)) | a)) by A3, A2, Th1;

          then

           A12: (x | a) in ( product ( Carrier (Aa,s9))) by Th2;

          consider Ji be non empty set, Cs be MSAlgebra-Family of Ji, S such that

           A13: Ji = (( id ( Class EqR)) . a) and

           A14: Cs = ((A / EqR) . a) & (A9 . a) = ( product Cs) by A7, Def5;

          Ji = a by A7, A13, FUNCT_1: 18;

          then (( Carrier (A9,s9)) . a) = ( product ( Carrier (Aa,s9))) by A8, A14, A9, PRALG_2:def 10;

          hence thesis by A4, A7, A12;

        end;

        take y;

        ( dom ( Carrier (( product (A / EqR)),s9))) = ( Class EqR) by PARTFUN1:def 2

        .= ( dom y) by PARTFUN1:def 2;

        then y in ( product ( Carrier (( product (A / EqR)),s9))) by A6, CARD_3: 9;

        hence thesis by A4, PRALG_2:def 10;

      end;

      consider F be ManySortedFunction of U19, U29 such that

       A15: for s be object st s in the carrier of S holds ex f be Function of (U19 . s), (U29 . s) st f = (F . s) & for x be object st x in (U19 . s) holds P[(f . x), x, s] from MSSUBFAM:sch 1( A1);

      

       A16: F is_homomorphism (U1,U2)

      proof

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

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

        thus ((F . ( the_result_sort_of o)) . (( Den (o,U1)) . x)) = (( Den (o,U2)) . (F # x))

        proof

          

           A17: (( Den (o,U1)) . x) in ( Result (o,U1));

          then

           A18: (( Den (o,U1)) . x) in (U19 . ( the_result_sort_of o)) by PRALG_2: 3;

          set s = ( the_result_sort_of o), U3 = ( product (A / EqR));

          

           A19: (U29 . s) = ( product ( Carrier (U3,s))) by PRALG_2:def 10;

          

           A20: ex f be Function of (U19 . s), (U29 . s) st f = (F . s) & for x9 be object st x9 in (U19 . s) holds P[(f . x9), x9, s] by A15;

          

           A21: ( dom (F . s)) = (( SORTS A) . s) by FUNCT_2:def 1

          .= ( product ( Carrier (A,s))) by PRALG_2:def 10;

          

           A22: (( Den (o,U1)) . x) in ( product ( Carrier (A,s))) by Th19;

          per cases ;

            suppose

             A23: ( the_arity_of o) = {} ;

            then ( Args (o,U1)) = { {} } by PRALG_2: 4;

            then

             A24: x = {} by TARSKI:def 1;

            then

             A25: ((F . s) . ( const (o,U1))) in ( rng (F . s)) by A21, A22, FUNCT_1:def 3;

            reconsider g1 = ((F . s) . ( const (o,U1))) as Function by A19;

            

             A26: ( dom ( const (o,U1))) = I by PARTFUN1:def 2, A22, A24;

             A27:

            now

              let e be Element of ( Class EqR);

              consider Ji be non empty set, Cs be MSAlgebra-Family of Ji, S such that

               A28: Ji = (( id ( Class EqR)) . e) and

               A29: Cs = ((A / EqR) . e) and

               A30: (U3 . e) = ( product Cs) by Def5;

              

               A31: ( dom (( const (o,( product A))) | e)) = (I /\ e) by A26, RELAT_1: 61

              .= e by XBOOLE_1: 28;

               A32:

              now

                let i1 be object;

                

                 A33: ( dom (A | e)) = (( dom A) /\ e) by RELAT_1: 61

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

                .= e by XBOOLE_1: 28;

                assume

                 A34: i1 in e;

                then

                reconsider ii = i1 as Element of Ji by A28;

                reconsider ii9 = ii as Element of I by A34;

                Cs = (A | e) by A29, Def4;

                then

                 A35: (Cs . ii) = (A . ii9) by A34, A33, FUNCT_1: 47;

                

                thus ((( const (o,( product A))) | e) . i1) = (( const (o,( product A))) . i1) by A31, A34, FUNCT_1: 47

                .= ( const (o,(A . ii9))) by A23, Th9

                .= (( const (o,( product Cs))) . i1) by A23, A35, Th9;

              end;

              ( const (o,( product Cs))) in ( Funcs (Ji,( union the set of all ( Result (o,(Cs . i9))) where i9 be Element of Ji))) by A23, Th8;

              then ( dom ( const (o,( product Cs)))) = e by A28, FUNCT_2: 92;

              hence (( const (o,U1)) | e) = ( const (o,(U3 . e))) by A30, A31, A32, FUNCT_1: 2;

            end;

            

             A36: ( const (o,U1)) in (U19 . ( the_result_sort_of o)) by A17, A24, PRALG_2: 3;

             A37:

            now

              let x1 be object;

              consider f1 be Function such that

               A38: f1 = ( const (o,U1));

              assume x1 in ( Class EqR);

              then

              reconsider e = x1 as Element of ( Class EqR);

              (g1 . e) = (f1 | e) by A20, A36, A38;

              

              hence (g1 . x1) = ( const (o,(U3 . e))) by A27, A38

              .= (( const (o,( product U3))) . x1) by A23, Th9;

            end;

            ( const (o,U2)) in ( Funcs (( Class EqR),( union the set of all ( Result (o,(U3 . i9))) where i9 be Element of ( Class EqR)))) by A23, Th8;

            then

             A39: ( dom ( const (o,U2))) = ( Class EqR) by FUNCT_2: 92;

            ( dom g1) = ( Class EqR) by PARTFUN1:def 2, A19, A25;

            then ((F . s) . ( const (o,U1))) = ( const (o,U2)) by A39, A37, FUNCT_1: 2;

            hence thesis by A23, A24, Th11;

          end;

            suppose

             A40: ( the_arity_of o) <> {} ;

            

             A41: (( Den (o,U2)) . (F # x)) in ( product ( Carrier (U3,s))) by Th19;

            then

            reconsider f1 = (( Den (o,U2)) . (F # x)) as Function;

            

             A42: ( dom f1) = ( Class EqR) by PARTFUN1:def 2, A41;

            

             A43: ((F . s) . (( Den (o,U1)) . x)) in ( rng (F . s)) by A21, A22, FUNCT_1:def 3;

            reconsider g1 = ((F . s) . (( Den (o,U1)) . x)) as Function by A19;

             A44:

            now

              let e be Element of ( Class EqR);

              consider Ji be non empty set, Cs be MSAlgebra-Family of Ji, S such that

               A45: Ji = (( id ( Class EqR)) . e) and

               A46: Cs = ((A / EqR) . e) and

               A47: (U3 . e) = ( product Cs) by Def5;

              

               A48: (( commute (F # x)) . e) is Element of ( Args (o,(U3 . e))) by A40, Th20;

              then

               A49: (( Den (o,(U3 . e))) . (( commute (F # x)) . e)) in ( product ( Carrier (Cs,s))) by A47, Th19;

              then

              reconsider f3 = (( Den (o,(U3 . e))) . (( commute (F # x)) . e)) as Function;

               A50:

              now

                let i1 be Element of I;

                assume

                 A51: i1 in e;

                then

                reconsider i2 = i1 as Element of Ji by A45;

                 A52:

                now

                  let n be object;

                  assume

                   A53: n in ( dom ( the_arity_of o));

                  then (( the_arity_of o) . n) in ( rng ( the_arity_of o)) by FUNCT_1:def 3;

                  then

                  reconsider s1 = (( the_arity_of o) . n) as SortSymbol of S;

                  

                   A54: (x . n) in ( product ( Carrier (A,(( the_arity_of o) /. n)))) by A53, Th15;

                  then

                  reconsider f4 = (x . n) as Function;

                  

                   A55: (x . n) in ( product ( Carrier (A,s1))) by A53, A54, PARTFUN1:def 6;

                  then

                   A56: (x . n) in (( SORTS A) . s1) by PRALG_2:def 10;

                  ( dom f4) = I by PARTFUN1:def 2, A55;

                  

                  then

                   A57: ( dom (f4 | e)) = (I /\ e) by RELAT_1: 61

                  .= e by XBOOLE_1: 28;

                  ((F # x) . n) in ( product ( Carrier (U3,(( the_arity_of o) /. n)))) by A53, Th15;

                  then

                  reconsider f5 = ((F # x) . n) as Function;

                  consider f7 be Function of (U19 . s1), (U29 . s1) such that

                   A58: f7 = (F . s1) and

                   A59: for x9 be object st x9 in (U19 . s1) holds P[(f7 . x9), x9, s1] by A15;

                  f5 = ((F . (( the_arity_of o) /. n)) . (x . n)) by A53, Th13

                  .= (f7 . (x . n)) by A53, A58, PARTFUN1:def 6;

                  then

                   A60: (f5 . e) = (f4 | e) by A56, A59;

                  then

                  reconsider f6 = (f5 . e) as Function;

                  f6 = ((( commute (F # x)) . e) . n) by A53, Th21;

                  

                  hence ((( commute (( commute (F # x)) . e)) . i1) . n) = ((f4 | e) . i2) by A47, A48, A53, A60, Th21

                  .= (f4 . i2) by A51, A57, FUNCT_1: 47

                  .= ((( commute x) . i1) . n) by A53, Th21;

                end;

                (( commute x) . i1) is Element of ( Args (o,(A . i1))) by A40, Th20;

                then (( commute x) . i1) in ( Args (o,(A . i1)));

                then (( commute x) . i1) in ( product (the Sorts of (A . i1) * ( the_arity_of o))) by PRALG_2: 3;

                

                then

                 A61: ( dom (( commute x) . i1)) = ( dom (the Sorts of (A . i1) * ( the_arity_of o))) by CARD_3: 9

                .= ( dom ( the_arity_of o)) by PRALG_2: 3;

                (( commute (( commute (F # x)) . e)) . i2) is Element of ( Args (o,(Cs . i2))) by A40, A47, A48, Th20;

                then (( commute (( commute (F # x)) . e)) . i2) in ( Args (o,(Cs . i2)));

                then (( commute (( commute (F # x)) . e)) . i2) in ( product (the Sorts of (Cs . i2) * ( the_arity_of o))) by PRALG_2: 3;

                

                then ( dom (( commute (( commute (F # x)) . e)) . i1)) = ( dom (the Sorts of (Cs . i2) * ( the_arity_of o))) by CARD_3: 9

                .= ( dom ( the_arity_of o)) by PRALG_2: 3;

                hence (( commute (( commute (F # x)) . e)) . i1) = (( commute x) . i1) by A61, A52;

              end;

              let f2 be Function such that

               A62: f2 = (( Den (o,U1)) . x);

              ( dom f2) = I by PARTFUN1:def 2, A22, A62;

              

              then

               A63: ( dom (f2 | e)) = (I /\ e) by RELAT_1: 61

              .= e by XBOOLE_1: 28;

              

               A64: (( commute (F # x)) . e) is Element of ( Args (o,( product Cs))) by A40, A47, Th20;

               A65:

              now

                let x1 be object;

                

                 A66: ( dom (A | e)) = (( dom A) /\ e) by RELAT_1: 61

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

                .= e by XBOOLE_1: 28;

                assume

                 A67: x1 in e;

                then

                reconsider i2 = x1 as Element of Ji by A45;

                reconsider i1 = i2 as Element of I by A67;

                Cs = (A | e) by A46, Def4;

                then (Cs . i2) = (A . i1) by A67, A66, FUNCT_1: 47;

                

                hence (f3 . x1) = (( Den (o,(A . i1))) . (( commute (( commute (F # x)) . e)) . i2)) by A40, A47, A64, Th22

                .= (( Den (o,(A . i1))) . (( commute x) . i1)) by A50, A67

                .= (f2 . x1) by A40, A62, Th22

                .= ((f2 | e) . x1) by A63, A67, FUNCT_1: 47;

              end;

              ( dom f3) = ( dom ( Carrier (Cs,s))) by A49, CARD_3: 9

              .= e by A45, PARTFUN1:def 2;

              hence (f2 | e) = (( Den (o,(U3 . e))) . (( commute (F # x)) . e)) by A63, A65, FUNCT_1: 2;

            end;

             A68:

            now

              reconsider f2 = (( Den (o,U1)) . x) as Function by A22;

              let x1 be object;

              assume x1 in ( Class EqR);

              then

              reconsider e = x1 as Element of ( Class EqR);

              (g1 . e) = (f2 | e) by A20, A18;

              

              hence (g1 . x1) = (( Den (o,(U3 . e))) . (( commute (F # x)) . e)) by A44

              .= (f1 . x1) by A40, Th22;

            end;

            ( dom g1) = ( Class EqR) by PARTFUN1:def 2, A19, A43;

            hence thesis by A42, A68, FUNCT_1: 2;

          end;

        end;

      end;

      F is "1-1"

      proof

        let s be set, g be Function such that

         A69: s in ( dom F) and

         A70: (F . s) = g;

        consider f be Function of (U19 . s), (U29 . s) such that

         A71: f = (F . s) and

         A72: for x be object st x in (U19 . s) holds P[(f . x), x, s] by A15, A69;

        let x1,x2 be object such that

         A73: x1 in ( dom g) and

         A74: x2 in ( dom g) and

         A75: (g . x1) = (g . x2);

        

         A76: ( dom f) = ( dom g) by A70, A71;

        thus x1 = x2

        proof

          reconsider s9 = s as SortSymbol of S by A69;

          

           A77: (U19 . s9) = ( product ( Carrier (A,s9))) by PRALG_2:def 10;

          then

           A78: ex gg be Function st x1 = gg & ( dom gg) = ( dom ( Carrier (A,s9))) & for x9 be object st x9 in ( dom ( Carrier (A,s9))) holds (gg . x9) in (( Carrier (A,s9)) . x9) by A73, A76, CARD_3:def 5;

          

           A79: ex gg1 be Function st x2 = gg1 & ( dom gg1) = ( dom ( Carrier (A,s9))) & for x9 be object st x9 in ( dom ( Carrier (A,s9))) holds (gg1 . x9) in (( Carrier (A,s9)) . x9) by A74, A76, A77, CARD_3:def 5;

          reconsider x2 as Function by A74, A76, A77;

          

           A80: ( dom x2) = I by A79, PARTFUN1:def 2;

          reconsider x1 as Function by A73, A76, A77;

          

           A81: (U29 . s) = ( product ( Carrier (( product (A / EqR)),s9))) by PRALG_2:def 10;

          

           A82: for i be object st i in I holds (x1 . i) = (x2 . i)

          proof

            reconsider f99 = (f . x2) as Function by A81;

            let i be object;

            assume

             A83: i in I;

            then

             A84: ( Class (EqR,i)) is Element of ( Class EqR) by EQREL_1:def 3;

            

            then (x1 | ( Class (EqR,i))) = (f99 . ( Class (EqR,i))) by A70, A73, A75, A71, A72, A76

            .= (x2 | ( Class (EqR,i))) by A74, A72, A76, A84;

            

            then (x1 . i) = ((x2 | ( Class (EqR,i))) . i) by A83, EQREL_1: 20, FUNCT_1: 49

            .= (x2 . i) by A83, EQREL_1: 20, FUNCT_1: 49;

            hence thesis;

          end;

          ( dom x1) = I by A78, PARTFUN1:def 2;

          hence thesis by A80, A82, FUNCT_1: 2;

        end;

      end;

      then

       A85: F is_monomorphism (U1,U2) by A16;

      F is "onto"

      proof

        let s be set such that

         A86: s in the carrier of S;

        reconsider s9 = s as SortSymbol of S by A86;

        consider f be Function of (U19 . s), (U29 . s) such that

         A87: f = (F . s) and

         A88: for x be object st x in (U19 . s) holds P[(f . x), x, s] by A15, A86;

        

         A89: (U19 . s9) = ( product ( Carrier (A,s9))) by PRALG_2:def 10;

        for y be object holds y in (U29 . s) iff ex x be object st x in ( dom f) & y = (f . x)

        proof

          let y be object;

          

           A90: y in (U29 . s) implies ex x be set st x in ( dom f) & y = (f . x)

          proof

            assume y in (U29 . s);

            then

             A91: y in ( product ( Carrier (( product (A / EqR)),s9))) by PRALG_2:def 10;

            then

             A92: ex gg be Function st y = gg & ( dom gg) = ( dom ( Carrier (( product (A / EqR)),s9))) & for x9 be object st x9 in ( dom ( Carrier (( product (A / EqR)),s9))) holds (gg . x9) in (( Carrier (( product (A / EqR)),s9)) . x9) by CARD_3:def 5;

            reconsider y as Function by A91;

            defpred Q[ object, object] means ex e be Element of ( Class EqR), f be Function st $1 in e & f = (y . e) & $2 = (f . $1);

            

             A93: for i be object st i in I holds ex j be object st Q[i, j]

            proof

              let i be object such that

               A94: i in I;

              ( Class (EqR,i)) in ( Class EqR) by A94, EQREL_1:def 3;

              then

              consider e be Element of ( Class EqR) such that

               A95: e = ( Class (EqR,i));

              consider Ji be non empty set, Cs be MSAlgebra-Family of Ji, S such that Ji = (( id ( Class EqR)) . e) and Cs = ((A / EqR) . e) and

               A96: (( product (A / EqR)) . e) = ( product Cs) by Def5;

              ex U0 be MSAlgebra over S st U0 = (( product (A / EqR)) . e) & (( Carrier (( product (A / EqR)),s9)) . e) = (the Sorts of U0 . s9) by PRALG_2:def 9;

              then ( dom ( Carrier (( product (A / EqR)),s9))) = ( Class EqR) & (( Carrier (( product (A / EqR)),s9)) . e) = ( product ( Carrier (Cs,s9))) by A96, PARTFUN1:def 2, PRALG_2:def 10;

              then

              reconsider y9 = (y . e) as Function by A92, Lm1;

               Q[i, (y9 . i)] by A94, A95, EQREL_1: 20;

              hence thesis;

            end;

            consider x be ManySortedSet of I such that

             A97: for i be object st i in I holds Q[i, (x . i)] from PBOOLE:sch 3( A93);

            

             A98: ( dom ( Carrier (( product (A / EqR)),s9))) = ( Class EqR) by PARTFUN1:def 2;

            

             A99: for z be object st z in ( dom ( Carrier (A,s9))) holds (x . z) in (( Carrier (A,s9)) . z)

            proof

              let z be object;

              assume z in ( dom ( Carrier (A,s9)));

              then z in I;

              then

              consider e be Element of ( Class EqR), f1 be Function such that

               A100: z in e and

               A101: f1 = (y . e) & (x . z) = (f1 . z) by A97;

              ( dom (( Carrier (A,s9)) | e)) = (( dom ( Carrier (A,s9))) /\ e) by RELAT_1: 61

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

              .= e by XBOOLE_1: 28;

              then

               A102: ((( Carrier (A,s9)) | e) . z) = (( Carrier (A,s9)) . z) by A100, FUNCT_1: 47;

              consider Ji be non empty set, Cs be MSAlgebra-Family of Ji, S such that

               A103: Ji = (( id ( Class EqR)) . e) and

               A104: Cs = ((A / EqR) . e) and

               A105: (( product (A / EqR)) . e) = ( product Cs) by Def5;

              Cs = (A | e) & Ji = e by A103, A104, Def4;

              then

               A106: ( Carrier (Cs,s9)) = (( Carrier (A,s9)) | e) by Th2;

              ex U0 be MSAlgebra over S st U0 = (( product (A / EqR)) . e) & (( Carrier (( product (A / EqR)),s9)) . e) = (the Sorts of U0 . s9) by PRALG_2:def 9;

              then

               A107: (( Carrier (( product (A / EqR)),s9)) . e) = ( product ( Carrier (Cs,s9))) by A105, PRALG_2:def 10;

              (y . e) in (( Carrier (( product (A / EqR)),s9)) . e) by A92, A98;

              then

               A108: ex g be Function st (y . e) = g & ( dom g) = ( dom ( Carrier (Cs,s9))) & for x9 be object st x9 in ( dom ( Carrier (Cs,s9))) holds (g . x9) in (( Carrier (Cs,s9)) . x9) by A107, CARD_3:def 5;

              ( dom ( Carrier (Cs,s9))) = e by A103, PARTFUN1:def 2;

              hence thesis by A100, A101, A108, A102, A106;

            end;

            ( dom x) = I by PARTFUN1:def 2

            .= ( dom ( Carrier (A,s9))) by PARTFUN1:def 2;

            then

             A109: x in (U19 . s9) by A89, A99, CARD_3: 9;

            then

             A110: x in ( dom f) by FUNCT_2:def 1;

            then (f . x) in ( rng f) by FUNCT_1:def 3;

            then (f . x) in (U29 . s);

            then

             A111: (f . x) in ( product ( Carrier (( product (A / EqR)),s9))) by PRALG_2:def 10;

            then

            reconsider f9 = (f . x) as Function;

            

             A112: for e be object st e in ( Class EqR) holds (y . e) = (f9 . e)

            proof

              let e be object;

              assume e in ( Class EqR);

              then

              reconsider e as Element of ( Class EqR);

              consider Ji be non empty set, Cs be MSAlgebra-Family of Ji, S such that

               A113: Ji = (( id ( Class EqR)) . e) and Cs = ((A / EqR) . e) and

               A114: (( product (A / EqR)) . e) = ( product Cs) by Def5;

              ex U0 be MSAlgebra over S st U0 = (( product (A / EqR)) . e) & (( Carrier (( product (A / EqR)),s9)) . e) = (the Sorts of U0 . s9) by PRALG_2:def 9;

              then

               A115: (( Carrier (( product (A / EqR)),s9)) . e) = ( product ( Carrier (Cs,s9))) by A114, PRALG_2:def 10;

              

               A116: (y . e) in (( Carrier (( product (A / EqR)),s9)) . e) by A92, A98;

              then

              reconsider y9 = (y . e) as Function by A115;

              

               A117: ( dom (x | e)) = (( dom x) /\ e) by RELAT_1: 61

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

              .= e by XBOOLE_1: 28;

              

               A118: for i be object st i in e holds ((x | e) . i) = (y9 . i)

              proof

                let i be object;

                assume

                 A119: i in e;

                then

                consider e1 be Element of ( Class EqR), f1 be Function such that

                 A120: i in e1 and

                 A121: f1 = (y . e1) & (x . i) = (f1 . i) by A97;

                e = e1 by A119, A120, Th3;

                hence thesis by A117, A119, A121, FUNCT_1: 47;

              end;

              ex g be Function st (y . e) = g & ( dom g) = ( dom ( Carrier (Cs,s9))) & for x9 be object st x9 in ( dom ( Carrier (Cs,s9))) holds (g . x9) in (( Carrier (Cs,s9)) . x9) by A116, A115, CARD_3:def 5;

              then ( dom y9) = e by A113, PARTFUN1:def 2;

              then (x | e) = y9 by A117, A118;

              hence thesis by A88, A109;

            end;

            ex gg9 be Function st (f . x) = gg9 & ( dom gg9) = ( dom ( Carrier (( product (A / EqR)),s9))) & for x9 be object st x9 in ( dom ( Carrier (( product (A / EqR)),s9))) holds (gg9 . x9) in (( Carrier (( product (A / EqR)),s9)) . x9) by A111, CARD_3:def 5;

            then y = f9 by A92, A112;

            hence thesis by A110;

          end;

          (ex x be set st x in ( dom f) & y = (f . x)) implies y in (U29 . s)

          proof

            given x be set such that

             A122: x in ( dom f) and

             A123: y = (f . x);

            (f . x) in ( rng f) by A122, FUNCT_1:def 3;

            hence thesis by A123;

          end;

          hence y in (U29 . s) iff ex x be object st x in ( dom f) & y = (f . x) by A90;

        end;

        hence thesis by A87, FUNCT_1:def 3;

      end;

      then F is_epimorphism (U1,U2) by A16;

      then F is_isomorphism (U1,U2) by A85;

      hence thesis;

    end;