equation.miz



    begin

    reserve I for set;

    theorem :: EQUATION:1

    

     Th1: for A be set, B,C be non empty set holds for f be Function of A, B, g be Function of B, C st ( rng (g * f)) = C holds ( rng g) = C

    proof

      let A be set, B,C be non empty set, f be Function of A, B, g be Function of B, C such that

       A1: ( rng (g * f)) = C;

      thus ( rng g) c= C;

      let q be object;

      assume q in C;

      then

      consider x be object such that

       A2: x in ( dom (g * f)) and

       A3: q = ((g * f) . x) by A1, FUNCT_1:def 3;

      

       A4: ( dom f) = A by FUNCT_2:def 1;

      then

       A5: (f . x) in ( rng f) by A2, FUNCT_1:def 3;

      ( dom (g * f)) = A by FUNCT_2:def 1;

      then

       A6: ( rng f) c= ( dom g) by A4, FUNCT_1: 15;

      q = (g . (f . x)) by A2, A3, FUNCT_1: 12;

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

    end;

    theorem :: EQUATION:2

    for A be ManySortedSet of I, B,C be non-empty ManySortedSet of I holds for f be ManySortedFunction of A, B, g be ManySortedFunction of B, C st (g ** f) is "onto" holds g is "onto"

    proof

      let A be ManySortedSet of I, B,C be non-empty ManySortedSet of I, f be ManySortedFunction of A, B, g be ManySortedFunction of B, C such that

       A1: (g ** f) is "onto";

      let i be set;

      assume

       A2: i in I;

      then

       A3: (f . i) is Function of (A . i), (B . i) & (g . i) is Function of (B . i), (C . i) by PBOOLE:def 15;

      ( rng ((g . i) * (f . i))) = ( rng ((g ** f) . i)) by A2, MSUALG_3: 2

      .= (C . i) by A1, A2;

      hence thesis by A2, A3, Th1;

    end;

    theorem :: EQUATION:3

    

     Th3: for A,B be non empty set, C,y be set holds for f be Function st f in ( Funcs (A,( Funcs (B,C)))) & y in B holds ( dom (( commute f) . y)) = A & ( rng (( commute f) . y)) c= C

    proof

      let A,B be non empty set, C,y be set, f be Function such that

       A1: f in ( Funcs (A,( Funcs (B,C)))) and

       A2: y in B;

      set cf = ( commute f);

      cf in ( Funcs (B,( Funcs (A,C)))) by A1, FUNCT_6: 55;

      then

       A3: ex g be Function st g = cf & ( dom g) = B & ( rng g) c= ( Funcs (A,C)) by FUNCT_2:def 2;

      then (cf . y) in ( rng cf) by A2, FUNCT_1:def 3;

      then ex t be Function st t = (( commute f) . y) & ( dom t) = A & ( rng t) c= C by A3, FUNCT_2:def 2;

      hence thesis;

    end;

    theorem :: EQUATION:4

    for A,B be ManySortedSet of I st A is_transformable_to B holds for f be ManySortedFunction of I st ( doms f) = A & ( rngs f) c= B holds f is ManySortedFunction of A, B

    proof

      let A,B be ManySortedSet of I such that for i be set st i in I holds (B . i) = {} implies (A . i) = {} ;

      let f be ManySortedFunction of I such that

       A1: ( doms f) = A and

       A2: ( rngs f) c= B;

      let i be object;

      assume

       A3: i in I;

      then

      reconsider J = I as non empty set;

      reconsider s = i as Element of J by A3;

      

       A4: ( dom (f . s)) = (A . s) by A1, MSSUBFAM: 14;

      ( rng (f . s)) = (( rngs f) . s) by MSSUBFAM: 13;

      then ( rng (f . s)) c= (B . s) by A2;

      hence thesis by A4, FUNCT_2: 2;

    end;

    theorem :: EQUATION:5

    

     Th5: for A,B be ManySortedSet of I, F be ManySortedFunction of A, B holds for C,E be ManySortedSubset of A, D be ManySortedSubset of C st E = D holds ((F || C) || D) = (F || E)

    proof

      let A,B be ManySortedSet of I, F be ManySortedFunction of A, B, C,E be ManySortedSubset of A, D be ManySortedSubset of C such that

       A1: E = D;

      now

        let i be object such that

         A2: i in I;

        D c= C by PBOOLE:def 18;

        then

         A4: (D . i) c= (C . i) by A2;

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

        then

        reconsider fc = ((F . i) | (C . i)) as Function of (C . i), (B . i) by A2, MSAFREE:def 1;

        

        thus (((F || C) || D) . i) = (((F || C) . i) | (D . i)) by A2, MSAFREE:def 1

        .= (fc | (D . i)) by A2, MSAFREE:def 1

        .= ((F . i) | (D . i)) by A4, RELAT_1: 74

        .= ((F || E) . i) by A1, A2, MSAFREE:def 1;

      end;

      hence thesis;

    end;

    theorem :: EQUATION:6

    

     Th6: for B be non-empty ManySortedSet of I, C be ManySortedSet of I holds for A be ManySortedSubset of C, F be ManySortedFunction of A, B holds ex G be ManySortedFunction of C, B st (G || A) = F

    proof

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

      defpred P[ object, object, object] means ex f be Function of (A . $3), (B . $3) st f = (F . $3) & ($2 in (A . $3) implies $1 = (f . $2));

      

       A1: for i be object st i in I holds for x be object st x in (C . i) holds ex y be object st y in (B . i) & P[y, x, i]

      proof

        let i be object;

        assume

         A2: i in I;

        then

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

        let x be object such that x in (C . i);

        per cases ;

          suppose

           A3: x in (A . i);

          take (f . x);

          thus (f . x) in (B . i) by A2, A3, FUNCT_2: 5;

          take f;

          thus thesis;

        end;

          suppose

           A4: not x in (A . i);

          consider y be object such that

           A5: y in (B . i) by A2, XBOOLE_0:def 1;

          take y;

          thus y in (B . i) by A5;

          take f;

          thus thesis by A4;

        end;

      end;

      consider G be ManySortedFunction of C, B such that

       A6: for i be object st i in I holds ex g be Function of (C . i), (B . i) st g = (G . i) & for x be object st x in (C . i) holds P[(g . x), x, i] from MSSUBFAM:sch 1( A1);

      take G;

      now

        let i be object;

        assume

         A7: i in I;

        then

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

        

         A8: ( dom f) = (A . i) by A7, FUNCT_2:def 1;

        consider g be Function of (C . i), (B . i) such that

         A9: g = (G . i) and

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

        A c= C by PBOOLE:def 18;

        then

         A11: (A . i) c= (C . i) by A7;

        

         A12: for x be object st x in (A . i) holds (f . x) = ((g | (A . i)) . x)

        proof

          let x be object;

          assume

           A13: x in (A . i);

          then ex h be Function of (A . i), (B . i) st h = (F . i) & (x in (A . i) implies (g . x) = (h . x)) by A10, A11;

          hence thesis by A13, FUNCT_1: 49;

        end;

        ( dom g) = (C . i) by A7, FUNCT_2:def 1;

        then

         A14: ( dom (g | (A . i))) = (A . i) by A11, RELAT_1: 62;

        

        thus ((G || A) . i) = (g | (A . i)) by A7, A9, MSAFREE:def 1

        .= (F . i) by A8, A14, A12, FUNCT_1: 2;

      end;

      hence thesis;

    end;

    definition

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

      :: EQUATION:def1

      func F "" A -> ManySortedSet of I means

      : Def1: for i be object st i in I holds (it . i) = ((F . i) " (A . i));

      existence

      proof

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

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

        hence thesis;

      end;

      uniqueness

      proof

        let X,Y be ManySortedSet of I such that

         A1: for i be object st i in I holds (X . i) = ((F . i) " (A . i)) and

         A2: for i be object st i in I holds (Y . i) = ((F . i) " (A . i));

        now

          let i be object;

          assume

           A3: i in I;

          

          hence (X . i) = ((F . i) " (A . i)) by A1

          .= (Y . i) by A2, A3;

        end;

        hence X = Y;

      end;

    end

    theorem :: EQUATION:7

    for A,B,C be ManySortedSet of I, F be ManySortedFunction of A, B holds (F .:.: C) is ManySortedSubset of B

    proof

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

      let i be object;

      assume

       A1: i in I;

      then

      reconsider J = I as non empty set;

      reconsider j = i as Element of J by A1;

      reconsider A1 = A, B1 = B as ManySortedSet of J;

      reconsider F1 = F as ManySortedFunction of A1, B1;

      ((F1 . j) .: (C . j)) c= (B . j);

      hence thesis by PBOOLE:def 20;

    end;

    theorem :: EQUATION:8

    for A,B,C be ManySortedSet of I, F be ManySortedFunction of A, B holds (F "" C) is ManySortedSubset of A

    proof

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

      let i be object;

      assume

       A1: i in I;

      then

      reconsider J = I as non empty set;

      reconsider j = i as Element of J by A1;

      reconsider A1 = A, B1 = B as ManySortedSet of J;

      reconsider F1 = F as ManySortedFunction of A1, B1;

      ((F1 . j) " (C . j)) c= (A . j);

      hence thesis by Def1;

    end;

    theorem :: EQUATION:9

    for A,B be ManySortedSet of I, F be ManySortedFunction of A, B st F is "onto" holds (F .:.: A) = B

    proof

      let A,B be ManySortedSet of I, F be ManySortedFunction of A, B such that

       A1: F is "onto";

      now

        let i be object;

        assume

         A2: i in I;

        then

         A3: (F . i) is Function of (A . i), (B . i) by PBOOLE:def 15;

        per cases ;

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

          

          thus ((F .:.: A) . i) = ((F . i) .: (A . i)) by A2, PBOOLE:def 20

          .= ( rng (F . i)) by A3, RELSET_1: 22

          .= (B . i) by A1, A2;

        end;

          suppose

           A4: not ((B . i) = {} implies (A . i) = {} );

          then

           A5: (F . i) = {} by A3;

          

          thus ((F .:.: A) . i) = ((F . i) .: (A . i)) by A2, PBOOLE:def 20

          .= (B . i) by A4, A5;

        end;

      end;

      hence thesis;

    end;

    theorem :: EQUATION:10

    for A,B be ManySortedSet of I, F be ManySortedFunction of A, B st A is_transformable_to B holds (F "" B) = A

    proof

      let A,B be ManySortedSet of I, F be ManySortedFunction of A, B such that

       A1: A is_transformable_to B;

      now

        let i be object;

        assume

         A2: i in I;

        then

         A3: (F . i) is Function of (A . i), (B . i) by PBOOLE:def 15;

        

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

        

        thus ((F "" B) . i) = ((F . i) " (B . i)) by A2, Def1

        .= (A . i) by A4, A3, FUNCT_2: 40;

      end;

      hence thesis;

    end;

    theorem :: EQUATION:11

    for A be ManySortedSet of I, F be ManySortedFunction of I st A c= ( rngs F) holds (F .:.: (F "" A)) = A

    proof

      let A be ManySortedSet of I, F be ManySortedFunction of I such that

       A1: A c= ( rngs F);

      now

        let i be object;

        assume

         A2: i in I;

        then (A . i) c= (( rngs F) . i) by A1;

        then

         A3: (A . i) c= ( rng (F . i)) by A2, MSSUBFAM: 13;

        

        thus ((F .:.: (F "" A)) . i) = ((F . i) .: ((F "" A) . i)) by A2, PBOOLE:def 20

        .= ((F . i) .: ((F . i) " (A . i))) by A2, Def1

        .= (A . i) by A3, FUNCT_1: 77;

      end;

      hence thesis;

    end;

    theorem :: EQUATION:12

    for f be ManySortedFunction of I holds for X be ManySortedSet of I holds (f .:.: X) c= ( rngs f)

    proof

      let f be ManySortedFunction of I;

      let X be ManySortedSet of I;

      let i be object;

      assume

       A1: i in I;

      then ((f .:.: X) . i) = ((f . i) .: (X . i)) by PBOOLE:def 20;

      then ((f .:.: X) . i) c= ( rng (f . i)) by RELAT_1: 111;

      hence thesis by A1, MSSUBFAM: 13;

    end;

    theorem :: EQUATION:13

    

     Th13: for f be ManySortedFunction of I holds (f .:.: ( doms f)) = ( rngs f)

    proof

      let f be ManySortedFunction of I;

      now

        let i be object;

        assume

         A1: i in I;

        

        hence ((f .:.: ( doms f)) . i) = ((f . i) .: (( doms f) . i)) by PBOOLE:def 20

        .= ((f . i) .: ( dom (f . i))) by A1, MSSUBFAM: 14

        .= ( rng (f . i)) by RELAT_1: 113

        .= (( rngs f) . i) by A1, MSSUBFAM: 13;

      end;

      hence thesis;

    end;

    theorem :: EQUATION:14

    

     Th14: for f be ManySortedFunction of I holds (f "" ( rngs f)) = ( doms f)

    proof

      let f be ManySortedFunction of I;

      now

        let i be object;

        assume

         A1: i in I;

        

        hence ((f "" ( rngs f)) . i) = ((f . i) " (( rngs f) . i)) by Def1

        .= ((f . i) " ( rng (f . i))) by A1, MSSUBFAM: 13

        .= ( dom (f . i)) by RELAT_1: 134

        .= (( doms f) . i) by A1, MSSUBFAM: 14;

      end;

      hence thesis;

    end;

    theorem :: EQUATION:15

    for A be ManySortedSet of I holds (( id A) .:.: A) = A

    proof

      let A be ManySortedSet of I;

      

       A1: ( rngs ( id A)) = A by EXTENS_1: 9;

      ( doms ( id A)) = A by MSSUBFAM: 17;

      hence thesis by A1, Th13;

    end;

    theorem :: EQUATION:16

    for A be ManySortedSet of I holds (( id A) "" A) = A

    proof

      let A be ManySortedSet of I;

      

       A1: ( rngs ( id A)) = A by EXTENS_1: 9;

      ( doms ( id A)) = A by MSSUBFAM: 17;

      hence thesis by A1, Th14;

    end;

    begin

    reserve S for non empty non void ManySortedSign,

U0,U1 for non-empty MSAlgebra over S;

    theorem :: EQUATION:17

    

     Th17: for A be MSAlgebra over S holds A is MSSubAlgebra of the MSAlgebra of A by MSUALG_2: 5;

    theorem :: EQUATION:18

    

     Th18: for U0 be MSAlgebra over S, A be MSSubAlgebra of U0 holds for o be OperSymbol of S, x be set st x in ( Args (o,A)) holds x in ( Args (o,U0))

    proof

      let U0 be MSAlgebra over S, A be MSSubAlgebra of U0, o be OperSymbol of S, x be set such that

       A1: x in ( Args (o,A));

      reconsider B0 = the Sorts of A as MSSubset of U0 by MSUALG_2:def 9;

       the MSAlgebra of U0 = the MSAlgebra of U0;

      then U0 is MSSubAlgebra of U0 by MSUALG_2: 5;

      then

      reconsider B1 = the Sorts of U0 as MSSubset of U0 by MSUALG_2:def 9;

      B0 c= B1 by PBOOLE:def 18;

      then (((B0 # ) * the Arity of S) . o) c= (((B1 # ) * the Arity of S) . o) by MSUALG_2: 2;

      hence thesis by A1;

    end;

    theorem :: EQUATION:19

    

     Th19: for U0 be MSAlgebra over S, A be MSSubAlgebra of U0 holds for o be OperSymbol of S, x be set st x in ( Args (o,A)) holds (( Den (o,A)) . x) = (( Den (o,U0)) . x)

    proof

      let U0 be MSAlgebra over S, A be MSSubAlgebra of U0, o be OperSymbol of S, x be set such that

       A1: x in ( Args (o,A));

      reconsider B = the Sorts of A as MSSubset of U0 by MSUALG_2:def 9;

      B is opers_closed by MSUALG_2:def 9;

      then

       A2: B is_closed_on o;

      

      thus (( Den (o,A)) . x) = ((( Opers (U0,B)) . o) . x) by MSUALG_2:def 9

      .= ((o /. B) . x) by MSUALG_2:def 8

      .= ((( Den (o,U0)) | (((B # ) * the Arity of S) . o)) . x) by A2, MSUALG_2:def 7

      .= (( Den (o,U0)) . x) by A1, FUNCT_1: 49;

    end;

    theorem :: EQUATION:20

    

     Th20: for F be MSAlgebra-Family of I, S, B be MSSubAlgebra of ( product F) holds for o be OperSymbol of S, x be object st x in ( Args (o,B)) holds (( Den (o,B)) . x) is Function & (( Den (o,( product F))) . x) is Function

    proof

      let F be MSAlgebra-Family of I, S, B be MSSubAlgebra of ( product F), o be OperSymbol of S, x be object;

      set r = ( the_result_sort_of o);

      assume

       A1: x in ( Args (o,B));

      then x in ( Args (o,( product F))) by Th18;

      then (( Den (o,( product F))) . x) in ( product ( Carrier (F,r))) by PRALG_3: 19;

      then (( Den (o,B)) . x) in ( product ( Carrier (F,r))) by A1, Th19;

      then

      reconsider p = (( Den (o,B)) . x) as Element of (( SORTS F) . r) by PRALG_2:def 10;

      

       A2: p is Function;

      hence (( Den (o,B)) . x) is Function;

      thus thesis by A1, A2, Th19;

    end;

    definition

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

      :: EQUATION:def2

      func SuperAlgebraSet B -> set means

      : Def2: for x be object holds x in it iff ex C be strict MSSubAlgebra of A st x = C & B is MSSubAlgebra of C;

      existence

      proof

        defpred P[ object] means ex C be strict MSSubAlgebra of A st $1 = C & B is MSSubAlgebra of C;

        consider IT be set such that

         A1: for x be object holds x in IT iff x in ( MSSub A) & P[x] from XBOOLE_0:sch 1;

        take IT;

        let x be object;

        thus x in IT implies ex C be strict MSSubAlgebra of A st x = C & B is MSSubAlgebra of C by A1;

        given C be strict MSSubAlgebra of A such that

         A2: x = C and

         A3: B is MSSubAlgebra of C;

        x in ( MSSub A) by A2, MSUALG_2:def 19;

        hence thesis by A1, A2, A3;

      end;

      uniqueness

      proof

        defpred P[ object] means ex C be strict MSSubAlgebra of A st $1 = C & B is MSSubAlgebra of C;

        for X1,X2 be set st (for x be object holds x in X1 iff P[x]) & (for x be object holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;

        hence thesis;

      end;

    end

    registration

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

      cluster ( SuperAlgebraSet B) -> non empty;

      coherence

      proof

         the MSAlgebra of B is MSSubAlgebra of B by MSUALG_2: 37;

        then

         A1: the MSAlgebra of B is MSSubAlgebra of A by MSUALG_2: 6;

        B is MSSubAlgebra of the MSAlgebra of B by Th17;

        hence thesis by A1, Def2;

      end;

    end

    registration

      let S be non empty non void ManySortedSign;

      cluster strict non-empty free for MSAlgebra over S;

      existence

      proof

        set X = the non-empty ManySortedSet of the carrier of S;

        take ( FreeMSA X);

        thus thesis;

      end;

    end

    registration

      let S be non empty non void ManySortedSign, A be non-empty MSAlgebra over S, X be non-empty finite-yielding MSSubset of A;

      cluster ( GenMSAlg X) -> finitely-generated;

      coherence

      proof

        per cases ;

          case S is non void;

          let S9 be non void non empty ManySortedSign such that

           A1: S9 = S;

          let H be MSAlgebra over S9;

          assume

           A2: H = ( GenMSAlg X);

          then

          reconsider T = X as MSSubset of H by A1, MSUALG_2:def 17;

          ( GenMSAlg T) = H by A1, A2, EXTENS_1: 18;

          then

          reconsider T as GeneratorSet of H by A1, A2, MSAFREE: 3;

          take T;

          thus thesis;

        end;

          case S is void;

          hence thesis;

        end;

      end;

    end

    registration

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

      cluster strict non-empty finitely-generated for MSSubAlgebra of A;

      existence

      proof

        set G = the non-empty finite-yielding ManySortedSubset of the Sorts of A;

        take ( GenMSAlg G);

        thus thesis;

      end;

    end

    registration

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

      cluster feasible for MSSubAlgebra of A;

      existence

      proof

         the MSAlgebra of A = the MSAlgebra of A;

        then

        reconsider B = A as MSSubAlgebra of A by MSUALG_2: 5;

        take B;

        thus thesis;

      end;

    end

    theorem :: EQUATION:21

    

     Th21: for A be MSAlgebra over S, C be MSSubAlgebra of A holds for D be ManySortedSubset of the Sorts of A st D = the Sorts of C holds for h be ManySortedFunction of A, U0 holds for g be ManySortedFunction of C, U0 st g = (h || D) holds for o be OperSymbol of S, x be Element of ( Args (o,A)) holds for y be Element of ( Args (o,C)) st ( Args (o,C)) <> {} & x = y holds (h # x) = (g # y)

    proof

      let A be MSAlgebra over S, C be MSSubAlgebra of A, D be ManySortedSubset of the Sorts of A such that

       A1: D = the Sorts of C;

      let h be ManySortedFunction of A, U0, g be ManySortedFunction of C, U0 such that

       A2: g = (h || D);

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

      let y be Element of ( Args (o,C)) such that

       A3: ( Args (o,C)) <> {} and

       A4: x = y;

      set hx = (h # x), gy = (g # y);

      set ar = ( the_arity_of o);

      

       A5: y in ( Args (o,A)) by A3, Th18;

      then

      reconsider xx = x, yy = y as Function by MSUALG_6: 1;

      

       A6: ( dom yy) = ( dom ar) by A3, MSUALG_3: 6;

      

       A7: ( dom xx) = ( dom ar) by A5, MSUALG_3: 6;

       A8:

      now

        let n be object;

        assume

         A9: n in ( dom ar);

        then

        reconsider n9 = n as Nat;

        reconsider hn = (h . (ar . n)) as Function of (the Sorts of A . (ar . n)), (the Sorts of U0 . (ar . n)) by A9, PARTFUN1: 4, PBOOLE:def 15;

        (ar . n) in the carrier of S by A9, PARTFUN1: 4;

        then

         A10: (g . (ar . n9)) = (hn | (D . (ar . n))) by A2, MSAFREE:def 1;

        ( dom (the Sorts of C * ( the_arity_of o))) = ( dom ar) by PARTFUN1:def 2;

        then (xx . n) in ((the Sorts of C * ar) . n) by A3, A4, A9, MSUALG_3: 6;

        then

         A11: (xx . n) in (D . (ar . n)) by A1, A9, FUNCT_1: 13;

        

        thus (hx . n) = (hx . n9)

        .= ((h . (ar /. n)) . (xx . n)) by A5, A7, A9, MSUALG_3: 24

        .= ((h . (ar . n)) . (xx . n)) by A9, PARTFUN1:def 6

        .= ((g . (ar . n)) . (xx . n)) by A10, A11, FUNCT_1: 49

        .= ((g . (ar /. n)) . (yy . n)) by A4, A9, PARTFUN1:def 6

        .= (gy . n9) by A3, A6, A9, MSUALG_3: 24

        .= (gy . n);

      end;

      ( dom hx) = ( dom ar) & ( dom gy) = ( dom ar) by MSUALG_3: 6;

      hence thesis by A8, FUNCT_1: 2;

    end;

    theorem :: EQUATION:22

    

     Th22: for A be feasible MSAlgebra over S, C be feasible MSSubAlgebra of A holds for D be ManySortedSubset of the Sorts of A st D = the Sorts of C holds for h be ManySortedFunction of A, U0 st h is_homomorphism (A,U0) holds for g be ManySortedFunction of C, U0 st g = (h || D) holds g is_homomorphism (C,U0)

    proof

      let A be feasible MSAlgebra over S, C be feasible MSSubAlgebra of A, D be ManySortedSubset of the Sorts of A such that

       A1: D = the Sorts of C;

      let h be ManySortedFunction of A, U0 such that

       A2: h is_homomorphism (A,U0);

      let g be ManySortedFunction of C, U0 such that

       A3: g = (h || D);

      let o be OperSymbol of S such that

       A4: ( Args (o,C)) <> {} ;

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

      reconsider y = x as Element of ( Args (o,A)) by A4, Th18;

      set r = ( the_result_sort_of o);

      

       A5: x in ( Args (o,A)) by A4, Th18;

      ( Result (o,C)) <> {} by A4, MSUALG_6:def 1;

      then (( Den (o,C)) . x) in ( Result (o,C)) by A4, FUNCT_2: 5;

      then

       A6: (( Den (o,C)) . x) in (the Sorts of C . (the ResultSort of S . o)) by FUNCT_2: 15;

      (( Den (o,A)) . x) = (( Den (o,C)) . x) by A4, Th19;

      

      hence ((g . ( the_result_sort_of o)) . (( Den (o,C)) . x)) = ((h . r) . (( Den (o,A)) . x)) by A1, A3, A6, INSTALG1: 39

      .= (( Den (o,U0)) . (h # y)) by A2, A5

      .= (( Den (o,U0)) . (g # x)) by A1, A3, A4, Th21;

    end;

    theorem :: EQUATION:23

    for B be strict non-empty MSAlgebra over S holds for G be GeneratorSet of U0, H be non-empty GeneratorSet of B holds for f be ManySortedFunction of U0, B st H c= (f .:.: G) & f is_homomorphism (U0,B) holds f is_epimorphism (U0,B)

    proof

      let B be strict non-empty MSAlgebra over S, G be GeneratorSet of U0, H be non-empty GeneratorSet of B, f be ManySortedFunction of U0, B such that

       A1: H c= (f .:.: G) and

       A2: f is_homomorphism (U0,B);

      reconsider I = the Sorts of ( Image f) as non-empty MSSubset of B by MSUALG_2:def 9;

      (f .:.: G) c= (f .:.: the Sorts of U0) by EXTENS_1: 2;

      then H c= (f .:.: the Sorts of U0) by A1, PBOOLE: 13;

      then H c= the Sorts of ( Image f) by A2, MSUALG_3:def 12;

      then H is ManySortedSubset of the Sorts of ( Image f) by PBOOLE:def 18;

      then

       A3: ( GenMSAlg H) is MSSubAlgebra of ( GenMSAlg I) by EXTENS_1: 17;

      reconsider I1 = the Sorts of ( Image f) as non-empty MSSubset of ( Image f) by PBOOLE:def 18;

      I is GeneratorSet of ( Image f) & ( GenMSAlg I) = ( GenMSAlg I1) by EXTENS_1: 18, MSAFREE2: 6;

      then ( GenMSAlg I) = ( Image f) by MSAFREE: 3;

      then B is MSSubAlgebra of ( Image f) by A3, MSAFREE: 3;

      then ( Image f) = B by MSUALG_2: 7;

      hence thesis by A2, MSUALG_3: 19;

    end;

    theorem :: EQUATION:24

    

     Th24: for W be strict free non-empty MSAlgebra over S holds for F be ManySortedFunction of U0, U1 st F is_epimorphism (U0,U1) holds for G be ManySortedFunction of W, U1 st G is_homomorphism (W,U1) holds ex H be ManySortedFunction of W, U0 st H is_homomorphism (W,U0) & G = (F ** H)

    proof

      let W be strict free non-empty MSAlgebra over S, F be ManySortedFunction of U0, U1 such that

       A1: F is_epimorphism (U0,U1);

      set sU0 = the Sorts of U0, sU1 = the Sorts of U1, I = the carrier of S;

      let G be ManySortedFunction of W, U1 such that

       A2: G is_homomorphism (W,U1);

      consider Gen be GeneratorSet of W such that

       A3: Gen is free by MSAFREE:def 6;

      defpred P[ object, object, object] means ex f be Function of (sU0 . $3), (sU1 . $3) st ex g be Function of (Gen . $3), (sU1 . $3) st f = (F . $3) & g = ((G || Gen) . $3) & $1 in (f " {(g . $2)});

      

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

      proof

        let i be object such that

         A5: i in I;

        reconsider g = ((G || Gen) . i) as Function of (Gen . i), (sU1 . i) by A5, PBOOLE:def 15;

        reconsider f = (F . i) as Function of (sU0 . i), (sU1 . i) by A5, PBOOLE:def 15;

        let x be object;

        assume x in (Gen . i);

        then

         A6: (g . x) in (sU1 . i) by A5, FUNCT_2: 5;

        F is "onto" by A1;

        then ( rng (F . i)) = (sU1 . i) by A5;

        then (f " {(g . x)}) <> {} by A6, FUNCT_2: 41;

        then

        consider y be object such that

         A7: y in (f " {(g . x)}) by XBOOLE_0:def 1;

        take y;

        thus y in (sU0 . i) by A7;

        thus thesis by A7;

      end;

      consider H be ManySortedFunction of Gen, sU0 such that

       A8: for i be object st i in I holds ex h be Function of (Gen . i), (sU0 . i) st h = (H . i) & for x be object st x in (Gen . i) holds P[(h . x), x, i] from MSSUBFAM:sch 1( A4);

      consider H1 be ManySortedFunction of W, U0 such that

       A9: H1 is_homomorphism (W,U0) and

       A10: (H1 || Gen) = H by A3;

      now

        let i be object;

        assume

         A11: i in I;

        then

        reconsider f9 = (F . i) as Function of (sU0 . i), (sU1 . i) by PBOOLE:def 15;

        reconsider g9 = ((G || Gen) . i) as Function of (Gen . i), (sU1 . i) by A11, PBOOLE:def 15;

        consider h be Function of (Gen . i), (sU0 . i) such that

         A12: h = (H . i) and

         A13: for x be object st x in (Gen . i) holds ex f be Function of (sU0 . i), (sU1 . i) st ex g be Function of (Gen . i), (sU1 . i) st f = (F . i) & g = ((G || Gen) . i) & (h . x) in (f " {(g . x)}) by A8, A11;

         A14:

        now

          let x be object;

          assume

           A15: x in (Gen . i);

          then

          consider f be Function of (sU0 . i), (sU1 . i), g be Function of (Gen . i), (sU1 . i) such that

           A16: f = (F . i) & g = ((G || Gen) . i) and

           A17: (h . x) in (f " {(g . x)}) by A13;

          (f . (h . x)) in {(g . x)} by A11, A17, FUNCT_2: 38;

          then (f . (h . x)) = (g . x) by TARSKI:def 1;

          hence ((f9 * h) . x) = (g9 . x) by A15, A16, A17, FUNCT_2: 15;

        end;

        (Gen . i) = ( dom g9) & (Gen . i) = ( dom (f9 * h)) by A11, FUNCT_2:def 1;

        then g9 = (f9 * h) by A14, FUNCT_1: 2;

        hence ((G || Gen) . i) = ((F ** H) . i) by A11, A12, MSUALG_3: 2;

      end;

      then (G || Gen) = (F ** (H1 || Gen)) by A10;

      then

       A18: (G || Gen) = ((F ** H1) || Gen) by EXTENS_1: 4;

      take H1;

      thus H1 is_homomorphism (W,U0) by A9;

      F is_homomorphism (U0,U1) by A1;

      then (F ** H1) is_homomorphism (W,U1) by A9, MSUALG_3: 10;

      hence thesis by A2, A18, EXTENS_1: 19;

    end;

    theorem :: EQUATION:25

    

     Th25: for I be non empty finite set, A be non-empty MSAlgebra over S holds for F be MSAlgebra-Family of I, S st for i be Element of I holds ex C be strict non-empty finitely-generated MSSubAlgebra of A st C = (F . i) holds ex B be strict non-empty finitely-generated MSSubAlgebra of A st for i be Element of I holds (F . i) is MSSubAlgebra of B

    proof

      let I be non empty finite set, A be non-empty MSAlgebra over S, F be MSAlgebra-Family of I, S such that

       A1: for i be Element of I holds ex C be strict non-empty finitely-generated MSSubAlgebra of A st C = (F . i);

      set Z = { C where C be Element of ( MSSub A) : ex i be Element of I, D be strict non-empty finitely-generated MSSubAlgebra of A st C = (F . i) & C = D };

      set J = the carrier of S;

      set m = the Element of I;

      consider W be strict non-empty finitely-generated MSSubAlgebra of A such that

       A2: W = (F . m) by A1;

      W is Element of ( MSSub A) by MSUALG_2:def 19;

      then W in Z by A2;

      then

      reconsider Z as non empty set;

      defpred P[ set, set] means ex Q be strict non-empty MSSubAlgebra of A, G be GeneratorSet of Q st $1 = Q & $2 = G & G is non-empty finite-yielding;

      

       A3: for a be Element of Z holds ex b be Element of ( Bool the Sorts of A) st P[a, b]

      proof

        let a be Element of Z;

        a in Z;

        then

        consider C be Element of ( MSSub A) such that

         A4: a = C and

         A5: ex i be Element of I, D be strict non-empty finitely-generated MSSubAlgebra of A st C = (F . i) & C = D;

        consider i be Element of I, D be strict non-empty finitely-generated MSSubAlgebra of A such that C = (F . i) and

         A6: C = D by A5;

        consider G be GeneratorSet of D such that

         A7: G is finite-yielding by MSAFREE2:def 10;

        consider S be non-empty finite-yielding ManySortedSubset of the Sorts of D such that

         A8: G c= S by A7, MSUALG_9: 7;

        the Sorts of D is MSSubset of A by MSUALG_2:def 9;

        then S c= the Sorts of D & the Sorts of D c= the Sorts of A by PBOOLE:def 18;

        then S c= the Sorts of A by PBOOLE: 13;

        then S is ManySortedSubset of the Sorts of A by PBOOLE:def 18;

        then

        reconsider b = S as Element of ( Bool the Sorts of A) by CLOSURE2:def 1;

        reconsider S as GeneratorSet of D by A8, MSSCYC_1: 21;

        take b, D;

        take S;

        thus a = D by A4, A6;

        thus thesis;

      end;

      consider f be Function of Z, ( Bool the Sorts of A) such that

       A9: for B be Element of Z holds P[B, (f . B)] from FUNCT_2:sch 3( A3);

      deffunc F( object) = ( union { a where a be Element of ( bool (the Sorts of A . $1)) : ex i be Element of I, K be ManySortedSet of J st K = (f . (F . i)) & a = (K . $1) });

      consider SOR be ManySortedSet of J such that

       A10: for j be object st j in J holds (SOR . j) = F(j) from PBOOLE:sch 4;

      SOR is ManySortedSubset of the Sorts of A

      proof

        let j be object such that

         A11: j in J;

        let q be object;

        set UU = { a where a be Element of ( bool (the Sorts of A . j)) : ex i be Element of I, K be ManySortedSet of J st K = (f . (F . i)) & a = (K . j) };

        assume q in (SOR . j);

        then q in ( union UU) by A10, A11;

        then

        consider w be set such that

         A12: q in w and

         A13: w in UU by TARSKI:def 4;

        consider a be Element of ( bool (the Sorts of A . j)) such that

         A14: w = a and ex i be Element of I, K be ManySortedSet of J st K = (f . (F . i)) & a = (K . j) by A13;

        thus thesis by A12, A14;

      end;

      then

      reconsider SOR as MSSubset of A;

      SOR is non-empty

      proof

        set i = the Element of I;

        consider C be strict non-empty finitely-generated MSSubAlgebra of A such that

         A15: C = (F . i) by A1;

        C is Element of ( MSSub A) by MSUALG_2:def 19;

        then

         A16: (F . i) in Z by A15;

        then

         A17: ex Q be strict non-empty MSSubAlgebra of A st ex G be GeneratorSet of Q st (F . i) = Q & (f . (F . i)) = G & G is non-empty finite-yielding by A9;

        then

        reconsider G1 = (f . (F . i)) as finite-yielding Element of ( Bool the Sorts of A) by A16, FUNCT_2: 5;

        let j be object such that

         A18: j in J;

        consider q be object such that

         A19: q in (G1 . j) by A18, A17, XBOOLE_0:def 1;

        set UU = { a where a be Element of ( bool (the Sorts of A . j)) : ex i be Element of I, K be ManySortedSet of J st K = (f . (F . i)) & a = (K . j) };

        G1 c= the Sorts of A by PBOOLE:def 18;

        then (G1 . j) c= (the Sorts of A . j) by A18;

        then (G1 . j) in UU;

        then q in ( union UU) by A19, TARSKI:def 4;

        hence thesis by A10, A18;

      end;

      then

      reconsider SOR as non-empty MSSubset of A;

       A20:

      now

        set i = the Element of I;

        let j be set such that

         A21: j in J;

        set UU = { a where a be Element of ( bool (the Sorts of A . j)) : ex i be Element of I, K be ManySortedSet of J st K = (f . (F . i)) & a = (K . j) };

        consider C be strict non-empty finitely-generated MSSubAlgebra of A such that

         A22: C = (F . i) by A1;

        C is Element of ( MSSub A) by MSUALG_2:def 19;

        then

         A23: (F . i) in Z by A22;

        then ex Q be strict non-empty MSSubAlgebra of A st ex G be GeneratorSet of Q st (F . i) = Q & (f . (F . i)) = G & G is non-empty finite-yielding by A9;

        then

        reconsider G1 = (f . (F . i)) as finite-yielding Element of ( Bool the Sorts of A) by A23, FUNCT_2: 5;

        G1 c= the Sorts of A by PBOOLE:def 18;

        then (G1 . j) c= (the Sorts of A . j) by A21;

        then (G1 . j) in UU;

        hence UU is non empty;

      end;

      SOR is finite-yielding

      proof

        let j be object such that

         A24: j in J;

        set UU = { a where a be Element of ( bool (the Sorts of A . j)) : ex i be Element of I, K be ManySortedSet of J st K = (f . (F . i)) & a = (K . j) };

        reconsider VV = UU as non empty set by A20, A24;

         A25:

        now

          defpred P[ set, set] means ex L be ManySortedSet of J st (f . (F . $1)) = L & $2 = (L . j);

          consider r be FinSequence such that

           A26: ( rng r) = I by FINSEQ_1: 52;

          

           A27: for a be Element of I holds ex b be Element of VV st P[a, b]

          proof

            let a be Element of I;

            consider W be strict non-empty finitely-generated MSSubAlgebra of A such that

             A28: W = (F . a) by A1;

            W is Element of ( MSSub A) by MSUALG_2:def 19;

            then

             A29: W in Z by A28;

            then ex Q be strict non-empty MSSubAlgebra of A st ex G be GeneratorSet of Q st W = Q & (f . W) = G & G is non-empty finite-yielding by A9;

            then

            reconsider G1 = (f . (F . a)) as finite-yielding Element of ( Bool the Sorts of A) by A28, A29, FUNCT_2: 5;

            G1 c= the Sorts of A by PBOOLE:def 18;

            then (G1 . j) c= (the Sorts of A . j) by A24;

            then (G1 . j) in UU;

            then

            reconsider b = (G1 . j) as Element of VV;

            take b, G1;

            thus thesis;

          end;

          consider h be Function of I, VV such that

           A30: for i be Element of I holds P[i, (h . i)] from FUNCT_2:sch 3( A27);

          

           A31: ( rng r) = ( dom h) by A26, FUNCT_2:def 1;

          then

          reconsider p = (h * r) as FinSequence by FINSEQ_1: 16;

          

           A32: VV c= ( rng p)

          proof

            let q be object;

            assume q in VV;

            then

            consider a be Element of ( bool (the Sorts of A . j)) such that

             A33: q = a and

             A34: ex i be Element of I, K be ManySortedSet of J st K = (f . (F . i)) & a = (K . j);

            consider i be Element of I, K be ManySortedSet of J such that

             A35: K = (f . (F . i)) & a = (K . j) by A34;

            

             A36: ( rng p) = ( rng h) & ( dom h) = I by A31, FUNCT_2:def 1, RELAT_1: 28;

            ex L be ManySortedSet of J st (f . (F . i)) = L & (h . i) = (L . j) by A30;

            hence thesis by A33, A35, A36, FUNCT_1:def 3;

          end;

          take p;

          ( rng p) c= ( rng h) by FUNCT_1: 14;

          then ( rng p) c= VV by XBOOLE_1: 1;

          hence ( rng p) = VV by A32;

        end;

        for x be set st x in UU holds x is finite

        proof

          let x be set;

          assume x in UU;

          then

          consider a be Element of ( bool (the Sorts of A . j)) such that

           A37: x = a and

           A38: ex w be Element of I, K be ManySortedSet of J st K = (f . (F . w)) & a = (K . j);

          consider w be Element of I, K be ManySortedSet of J such that

           A39: K = (f . (F . w)) & a = (K . j) by A38;

          

           A40: ex E be strict non-empty finitely-generated MSSubAlgebra of A st E = (F . w) by A1;

          then (F . w) is Element of ( MSSub A) by MSUALG_2:def 19;

          then (F . w) in Z by A40;

          then P[(F . w), (f . (F . w))] by A9;

          hence thesis by A37, A39;

        end;

        then ( union UU) is finite by A25, FINSET_1: 7;

        hence thesis by A10, A24;

      end;

      then

      reconsider SOR as non-empty finite-yielding MSSubset of A;

      take ( GenMSAlg SOR);

      let i be Element of I;

      consider C be strict non-empty finitely-generated MSSubAlgebra of A such that

       A41: C = (F . i) by A1;

      C is Element of ( MSSub A) by MSUALG_2:def 19;

      then (F . i) in Z by A41;

      then

      consider Q be strict non-empty MSSubAlgebra of A, G be GeneratorSet of Q such that

       A42: (F . i) = Q and

       A43: (f . (F . i)) = G and

       A44: G is non-empty finite-yielding by A9;

      the Sorts of Q is MSSubset of A by MSUALG_2:def 9;

      then G c= the Sorts of Q & the Sorts of Q c= the Sorts of A by PBOOLE:def 18;

      then

       A45: G c= the Sorts of A by PBOOLE: 13;

      then

      reconsider G1 = G as non-empty MSSubset of A by A44, PBOOLE:def 18;

      

       A46: G1 is ManySortedSubset of SOR

      proof

        let j be object such that

         A47: j in J;

        set UU = { a where a be Element of ( bool (the Sorts of A . j)) : ex i be Element of I, K be ManySortedSet of J st K = (f . (F . i)) & a = (K . j) };

        (G1 . j) c= (the Sorts of A . j) by A45, A47;

        then

         A48: (G1 . j) in UU by A43;

        let q be object;

        assume q in (G1 . j);

        then q in ( union UU) by A48, TARSKI:def 4;

        hence thesis by A10, A47;

      end;

      C = ( GenMSAlg G) by A41, A42, MSAFREE: 3

      .= ( GenMSAlg G1) by EXTENS_1: 18;

      hence thesis by A41, A46, EXTENS_1: 17;

    end;

    theorem :: EQUATION:26

    

     Th26: for A,B be strict non-empty finitely-generated MSSubAlgebra of U0 holds ex M be strict non-empty finitely-generated MSSubAlgebra of U0 st A is MSSubAlgebra of M & B is MSSubAlgebra of M

    proof

      let A,B be strict non-empty finitely-generated MSSubAlgebra of U0;

      ( len <%A, B%>) = 2 by AFINSQ_1: 38;

      then ( dom <%A, B%>) = { 0 , 1} by CARD_1: 50;

      then

      reconsider F = <%A, B%> as ManySortedSet of { 0 , 1} by RELAT_1:def 18, PARTFUN1:def 2;

      

       A1: (F . 1) = B;

      

       A2: (F . 0 ) = A;

      F is MSAlgebra-Family of { 0 , 1}, S

      proof

        let i be object;

        assume i in { 0 , 1};

        hence thesis by A1, TARSKI:def 2, A2;

      end;

      then

      reconsider F as MSAlgebra-Family of { 0 , 1}, S;

      for i be Element of { 0 , 1} holds ex C be strict non-empty finitely-generated MSSubAlgebra of U0 st C = (F . i)

      proof

        let i be Element of { 0 , 1};

        per cases by TARSKI:def 2;

          suppose

           A3: i = 0 ;

          take A;

          thus thesis by A3;

        end;

          suppose

           A4: i = 1;

          take B;

          thus thesis by A4;

        end;

      end;

      then

      consider M be strict non-empty finitely-generated MSSubAlgebra of U0 such that

       A5: for i be Element of { 0 , 1} holds (F . i) is MSSubAlgebra of M by Th25;

      take M;

       0 in { 0 , 1} by TARSKI:def 2;

      hence A is MSSubAlgebra of M by A5, A2;

      1 in { 0 , 1} by TARSKI:def 2;

      hence thesis by A5, A1;

    end;

    theorem :: EQUATION:27

    for SG be non empty non void ManySortedSign holds for AG be non-empty MSAlgebra over SG holds for C be set st C = { A where A be Element of ( MSSub AG) : ex R be strict non-empty finitely-generated MSSubAlgebra of AG st R = A } holds for F be MSAlgebra-Family of C, SG st for c be object st c in C holds c = (F . c) holds ex PS be strict non-empty MSSubAlgebra of ( product F), BA be ManySortedFunction of PS, AG st BA is_epimorphism (PS,AG)

    proof

      let SG be non empty non void ManySortedSign, AG be non-empty MSAlgebra over SG, C be set such that

       A1: C = { A where A be Element of ( MSSub AG) : ex R be strict non-empty finitely-generated MSSubAlgebra of AG st R = A };

       A2:

      now

        let A be strict non-empty finitely-generated MSSubAlgebra of AG;

        A in ( MSSub AG) by MSUALG_2:def 19;

        hence A in C by A1;

      end;

      then

      reconsider CC = C as non empty set;

      set T = the strict non-empty finitely-generated MSSubAlgebra of AG;

      set I = the carrier of SG;

      let F be MSAlgebra-Family of C, SG such that

       A3: for c be object st c in C holds c = (F . c);

      reconsider FF = F as MSAlgebra-Family of CC, SG;

      set pr = ( product FF);

      defpred T[ object, object] means ex t be SortSymbol of SG, f be Element of (( SORTS FF) . t) st ex A be strict non-empty finitely-generated MSSubAlgebra of AG st t = $1 & f = $2 & for B be strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds (f . A) = (f . B);

      consider SOR be ManySortedSet of I such that

       A4: for i be object st i in I holds for e be object holds e in (SOR . i) iff e in (( SORTS FF) . i) & T[i, e] from PBOOLE:sch 2;

      SOR is MSSubset of pr

      proof

        let i be object such that

         A5: i in I;

        let e be object;

        assume e in (SOR . i);

        hence thesis by A4, A5;

      end;

      then

      reconsider SOR as MSSubset of pr;

      SOR is opers_closed

      proof

        let o be OperSymbol of SG;

        set r = ( the_result_sort_of o);

        set ar = ( the_arity_of o);

        let q be object such that

         A6: q in ( rng (( Den (o,pr)) | (((SOR # ) * the Arity of SG) . o)));

        reconsider q1 = q as Element of (( SORTS FF) . r) by A6, PRALG_2: 3;

        consider g be object such that

         A7: g in ( dom (( Den (o,pr)) | (((SOR # ) * the Arity of SG) . o))) and

         A8: q = ((( Den (o,pr)) | (((SOR # ) * the Arity of SG) . o)) . g) by A6, FUNCT_1:def 3;

        

         A9: q = (( Den (o,pr)) . g) by A7, A8, FUNCT_1: 47;

        

         A10: g in (((SOR # ) * the Arity of SG) . o) by A7;

        g in ( dom ( Den (o,pr))) by A7, RELAT_1: 57;

        then

        reconsider g as Element of ( Args (o,pr));

         T[r, q]

        proof

          take r;

          take q1;

          per cases ;

            suppose

             A11: ( the_arity_of o) = {} ;

            set A = the strict non-empty finitely-generated MSSubAlgebra of AG;

            ( Args (o,A)) = { {} } by A11, PRALG_2: 4;

            then

             A12: {} in ( Args (o,A)) by TARSKI:def 1;

            take A;

            thus r = r;

            thus q1 = q;

            let B be strict non-empty finitely-generated MSSubAlgebra of AG such that A is MSSubAlgebra of B;

            ( Args (o,B)) = { {} } by A11, PRALG_2: 4;

            then

             A13: {} in ( Args (o,B)) by TARSKI:def 1;

            B in ( MSSub AG) by MSUALG_2:def 19;

            then

             A14: B in CC by A1;

            A in ( MSSub AG) by MSUALG_2:def 19;

            then A in CC by A1;

            then

            reconsider iA = A, iB = B as Element of CC by A14;

            

             A15: iA = (FF . iA) by A3;

            

             A16: iB = (FF . iB) by A3;

            ( Args (o,pr)) = { {} } by A11, PRALG_2: 4;

            then

             A17: g = {} by TARSKI:def 1;

            

            hence (q1 . A) = (( const (o,pr)) . iA) by A9, PRALG_3:def 1

            .= ( const (o,(FF . iA))) by A11, PRALG_3: 9

            .= (( Den (o,(FF . iA))) . {} ) by PRALG_3:def 1

            .= (( Den (o,AG)) . {} ) by A15, A12, Th19

            .= (( Den (o,(FF . iB))) . {} ) by A16, A13, Th19

            .= ( const (o,(FF . iB))) by PRALG_3:def 1

            .= (( const (o,pr)) . iB) by A11, PRALG_3: 9

            .= (q1 . B) by A9, A17, PRALG_3:def 1;

          end;

            suppose

             A18: ( the_arity_of o) <> {} ;

            then

            reconsider domar = ( dom ar) as non empty finite set;

            defpred P[ set, set] means ex gn be Function, A be strict non-empty finitely-generated MSSubAlgebra of AG st gn = (g . $1) & (for B be strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds (gn . A) = (gn . B)) & $2 = A;

            g in ((SOR # ) . (the Arity of SG . o)) by A10, FUNCT_2: 15;

            then

             A19: g in ( product (SOR * ar)) by FINSEQ_2:def 5;

            

            then

             A20: ( dom (SOR * ar)) = ( dom g) by CARD_3: 9

            .= domar by MSUALG_3: 6;

            

             A21: for a be Element of domar holds ex b be Element of ( MSSub AG) st P[a, b]

            proof

              let n be Element of domar;

              (g . n) in ((SOR * ar) . n) by A19, A20, CARD_3: 9;

              then (ar . n) in I & (g . n) in (SOR . (ar . n)) by FUNCT_1: 13, PARTFUN1: 4;

              then

              consider s be SortSymbol of SG, f be Element of (( SORTS FF) . s), A be strict non-empty finitely-generated MSSubAlgebra of AG such that s = (ar . n) and

               A22: f = (g . n) and

               A23: for B be strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds (f . A) = (f . B) by A4;

              reconsider b = A as Element of ( MSSub AG) by MSUALG_2:def 19;

              take b, f;

              take A;

              thus f = (g . n) by A22;

              thus for B be strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds (f . A) = (f . B) by A23;

              thus thesis;

            end;

            consider KK be Function of domar, ( MSSub AG) such that

             A24: for n be Element of domar holds P[n, (KK . n)] from FUNCT_2:sch 3( A21);

            reconsider KK as ManySortedSet of domar;

            KK is MSAlgebra-Family of domar, SG

            proof

              let n be object;

              assume n in domar;

              then ex gn be Function st ex A be strict non-empty finitely-generated MSSubAlgebra of AG st gn = (g . n) & (for B be strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds (gn . A) = (gn . B)) & (KK . n) = A by A24;

              hence thesis;

            end;

            then

            reconsider KK as MSAlgebra-Family of domar, SG;

            for n be Element of domar holds ex C be strict non-empty finitely-generated MSSubAlgebra of AG st C = (KK . n)

            proof

              let n be Element of domar;

              ex gn be Function, A be strict non-empty finitely-generated MSSubAlgebra of AG st gn = (g . n) & (for B be strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds (gn . A) = (gn . B)) & (KK . n) = A by A24;

              hence thesis;

            end;

            then

            consider K be strict non-empty finitely-generated MSSubAlgebra of AG such that

             A25: for n be Element of domar holds (KK . n) is MSSubAlgebra of K by Th25;

            take K;

            thus r = r;

            thus q1 = q;

            let B be strict non-empty finitely-generated MSSubAlgebra of AG such that

             A26: K is MSSubAlgebra of B;

            K in ( MSSub AG) by MSUALG_2:def 19;

            then

             A27: K in CC by A1;

            B in ( MSSub AG) by MSUALG_2:def 19;

            then B in CC by A1;

            then

            reconsider iB = B, iK = K as Element of CC by A27;

            

             A28: g in ( Funcs (( dom ar),( Funcs (CC,( union the set of all (the Sorts of (FF . i) . s) where i be Element of CC, s be Element of the carrier of SG))))) by PRALG_3: 14;

            then

             A29: ( dom (( commute g) . iB)) = domar by Th3;

            

             A30: ( dom (( commute g) . iK)) = domar by A28, Th3;

            

             A31: for n be object st n in ( dom (( commute g) . iK)) holds ((( commute g) . iB) . n) = ((( commute g) . iK) . n)

            proof

              let x be object;

              assume

               A32: x in ( dom (( commute g) . iK));

              then

              consider gn be Function, A be strict non-empty finitely-generated MSSubAlgebra of AG such that

               A33: gn = (g . x) and

               A34: (for B be strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds (gn . A) = (gn . B)) & (KK . x) = A by A24, A30;

              

               A35: (KK . x) is MSSubAlgebra of K by A25, A30, A32;

              

              thus ((( commute g) . iB) . x) = (gn . iB) by A30, A32, A33, PRALG_3: 21

              .= (gn . A) by A26, A34, A35, MSUALG_2: 6

              .= (gn . iK) by A25, A30, A32, A34

              .= ((( commute g) . iK) . x) by A30, A32, A33, PRALG_3: 21;

            end;

            

             A36: iK = (FF . iK) by A3;

            

             A37: (( commute g) . iK) is Element of ( Args (o,(FF . iK))) by A18, PRALG_3: 20;

            

             A38: (( commute g) . iB) is Element of ( Args (o,(FF . iB))) by A18, PRALG_3: 20;

            

             A39: iB = (FF . iB) by A3;

            

            thus (q1 . K) = (( Den (o,(FF . iK))) . (( commute g) . iK)) by A9, A18, PRALG_3: 22

            .= (( Den (o,AG)) . (( commute g) . iK)) by A36, A37, Th19

            .= (( Den (o,AG)) . (( commute g) . iB)) by A28, A29, A31, Th3, FUNCT_1: 2

            .= (( Den (o,(FF . iB))) . (( commute g) . iB)) by A39, A38, Th19

            .= (q1 . B) by A9, A18, PRALG_3: 22;

          end;

        end;

        then q in (SOR . r) by A4;

        hence thesis by FUNCT_2: 15;

      end;

      then

       A40: (pr | SOR) = MSAlgebra (# SOR, ( Opers (pr,SOR)) #) by MSUALG_2:def 15;

      defpred Z[ object, object, object] means ex s be SortSymbol of SG, f be Element of (( SORTS FF) . s) st ex A be strict non-empty finitely-generated MSSubAlgebra of AG st s = $3 & f = $2 & (for B be strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds (f . A) = (f . B)) & $1 = (f . A);

      SOR is non-empty

      proof

        defpred P[ object] means ex C be strict non-empty MSSubAlgebra of AG st $1 = C & C is finitely-generated;

        let i be object;

        consider ST1 be set such that

         A41: for x be object holds x in ST1 iff x in ( SuperAlgebraSet T) & P[x] from XBOOLE_0:sch 1;

        

         A42: ST1 c= CC

        proof

          let q be object;

          assume q in ST1;

          then

           A43: ex C be strict non-empty MSSubAlgebra of AG st q = C & C is finitely-generated by A41;

          then q in ( MSSub AG) by MSUALG_2:def 19;

          hence thesis by A1, A43;

        end;

        defpred A[ object, object] means ex K be MSSubAlgebra of AG st ex t be set st $1 = K & t in (the Sorts of K . i) & $2 = t;

        assume

         A44: i in I;

        then

        consider x be object such that

         A45: x in (the Sorts of T . i) by XBOOLE_0:def 1;

        reconsider s = i as SortSymbol of SG by A44;

        

         A46: for c be object st c in CC holds ex j be object st A[c, j]

        proof

          let c be object;

          assume c in CC;

          then

          consider C be Element of ( MSSub AG) such that

           A47: c = C and

           A48: ex R be strict non-empty finitely-generated MSSubAlgebra of AG st R = C by A1;

          consider R be strict non-empty finitely-generated MSSubAlgebra of AG such that

           A49: R = C by A48;

          consider t be object such that

           A50: t in (the Sorts of R . i) by A44, XBOOLE_0:def 1;

          take t, R;

          reconsider t as set by TARSKI: 1;

          take t;

          thus c = R by A47, A49;

          thus thesis by A50;

        end;

        consider f be ManySortedSet of CC such that

         A51: for c be object st c in CC holds A[c, (f . c)] from PBOOLE:sch 3( A46);

        set g = (f +* (ST1 --> x));

        

         A52: ( dom (ST1 --> x)) = ST1;

        

         A53: for a be object st a in ( dom ( Carrier (FF,s))) holds (g . a) in (( Carrier (FF,s)) . a)

        proof

          let a be object;

          assume a in ( dom ( Carrier (FF,s)));

          then

           A54: a in CC;

          then

           A55: ex U0 be MSAlgebra over SG st U0 = (FF . a) & (( Carrier (FF,s)) . a) = (the Sorts of U0 . s) by PRALG_2:def 9;

          consider K be MSSubAlgebra of AG, t be set such that

           A56: a = K & t in (the Sorts of K . i) and

           A57: (f . a) = t by A51, A54;

          per cases ;

            suppose

             A58: a in ST1;

            then a in ( dom (ST1 --> x));

            then (g . a) = ((ST1 --> x) . a) by FUNCT_4: 13;

            then

             A59: (g . a) = x by A58, FUNCOP_1: 7;

            a in ( SuperAlgebraSet T) by A41, A58;

            then

            consider M be strict MSSubAlgebra of AG such that

             A60: a = M and

             A61: T is MSSubAlgebra of M by Def2;

            the Sorts of T is ManySortedSubset of the Sorts of M by A61, MSUALG_2:def 9;

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

            then (the Sorts of T . i) c= (the Sorts of M . i) by A44;

            then x in (the Sorts of M . i) by A45;

            hence thesis by A3, A54, A55, A59, A60;

          end;

            suppose not a in ST1;

            then (g . a) = t by A52, A57, FUNCT_4: 11;

            hence thesis by A3, A54, A55, A56;

          end;

        end;

        ( dom g) = (( dom f) \/ ( dom (ST1 --> x))) by FUNCT_4:def 1

        .= (CC \/ ( dom (ST1 --> x))) by PARTFUN1:def 2

        .= (CC \/ ST1)

        .= CC by A42, XBOOLE_1: 12

        .= ( dom ( Carrier (FF,s))) by PARTFUN1:def 2;

        then

         A62: g in ( product ( Carrier (FF,s))) by A53, CARD_3: 9;

         T[i, g]

        proof

          reconsider g1 = g as Element of (( SORTS FF) . s) by A62, PRALG_2:def 10;

          take s;

          take g1;

          take T;

          thus s = i;

          thus g1 = g;

          let B be strict non-empty finitely-generated MSSubAlgebra of AG;

          assume T is MSSubAlgebra of B;

          then B in ( SuperAlgebraSet T) by Def2;

          then

           A63: B in ST1 by A41;

          T is MSSubAlgebra of T by MSUALG_2: 5;

          then T in ( SuperAlgebraSet T) by Def2;

          then

           A64: T in ST1 by A41;

          

          hence (g1 . T) = ((ST1 --> x) . T) by A52, FUNCT_4: 13

          .= x by A64, FUNCOP_1: 7

          .= ((ST1 --> x) . B) by A63, FUNCOP_1: 7

          .= (g1 . B) by A52, A63, FUNCT_4: 13;

        end;

        hence thesis by A4;

      end;

      then

      reconsider PS = (pr | SOR) as strict non-empty MSSubAlgebra of ( product F) by A40, MSUALG_1:def 3;

       A65:

      now

        let s be SortSymbol of SG, f be Element of (( SORTS FF) . s), A be strict non-empty finitely-generated MSSubAlgebra of AG;

        

         A66: ( dom ( Carrier (FF,s))) = CC by PARTFUN1:def 2;

        A in ( MSSub AG) by MSUALG_2:def 19;

        then

         A67: A in ( dom ( Carrier (FF,s))) by A1, A66;

        then

        consider U0 be MSAlgebra over SG such that

         A68: U0 = (FF . A) and

         A69: (( Carrier (FF,s)) . A) = (the Sorts of U0 . s) by PRALG_2:def 9;

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

        then

         A70: (f . A) in (( Carrier (FF,s)) . A) by A67, CARD_3: 9;

        (FF . A) = A by A3, A67;

        then the Sorts of U0 is ManySortedSubset of the Sorts of AG by A68, MSUALG_2:def 9;

        then the Sorts of U0 c= the Sorts of AG by PBOOLE:def 18;

        then (the Sorts of U0 . s) c= (the Sorts of AG . s);

        hence (f . A) in (the Sorts of AG . s) by A69, A70;

      end;

       A71:

      now

        let i be object such that

         A72: i in I;

        let x be object;

        assume x in (the Sorts of PS . i);

        then

        consider s be SortSymbol of SG, f be Element of (( SORTS FF) . s), A be strict non-empty finitely-generated MSSubAlgebra of AG such that

         A73: s = i and

         A74: f = x & for B be strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds (f . A) = (f . B) by A4, A40, A72;

        reconsider y = (f . A) as object;

        take y;

        thus y in (the Sorts of AG . i) by A65, A73;

        thus Z[y, x, i] by A73, A74;

      end;

      consider BA be ManySortedFunction of PS, AG such that

       A75: for i be object st i in I holds ex g be Function of (the Sorts of PS . i), (the Sorts of AG . i) st g = (BA . i) & for x be object st x in (the Sorts of PS . i) holds Z[(g . x), x, i] from MSSUBFAM:sch 1( A71);

      take PS;

      take BA;

      thus BA is_homomorphism (PS,AG)

      proof

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

        let k be Element of ( Args (o,PS));

        set r = ( the_result_sort_of o), ar = ( the_arity_of o);

        consider g be Function of (the Sorts of PS . r), (the Sorts of AG . r) such that

         A76: g = (BA . r) and

         A77: for k be object st k in (the Sorts of PS . r) holds Z[(g . k), k, r] by A75;

        consider s be SortSymbol of SG, f be Element of (( SORTS FF) . s), A be strict non-empty finitely-generated MSSubAlgebra of AG such that s = r and

         A78: f = (( Den (o,PS)) . k) and

         A79: for B be strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds (f . A) = (f . B) and

         A80: (g . (( Den (o,PS)) . k)) = (f . A) by A77, MSUALG_9: 18;

        per cases ;

          suppose

           A81: ( the_arity_of o) = {} ;

          A in ( MSSub AG) by MSUALG_2:def 19;

          then A in CC by A1;

          then

          reconsider iA = A as Element of CC;

          reconsider ff1 = (( Den (o,pr)) . k) as Function by Th20;

          

           A82: (( Den (o,pr)) . {} ) = ( const (o,pr)) by PRALG_3:def 1;

          ( Args (o,A)) = { {} } by A81, PRALG_2: 4;

          then

           A83: {} in ( Args (o,A)) by TARSKI:def 1;

          

           A84: ( Args (o,PS)) = { {} } by A81, PRALG_2: 4;

          then

           A85: k = {} by TARSKI:def 1;

          

          thus ((BA . ( the_result_sort_of o)) . (( Den (o,PS)) . k)) = (ff1 . A) by A76, A78, A80, Th19

          .= (( const (o,pr)) . iA) by A84, A82, TARSKI:def 1

          .= ( const (o,(FF . iA))) by A81, PRALG_3: 9

          .= (( Den (o,(FF . iA))) . {} ) by PRALG_3:def 1

          .= (( Den (o,A)) . {} ) by A3

          .= (( Den (o,AG)) . {} ) by A83, Th19

          .= (( Den (o,AG)) . (BA # k)) by A81, A85, PRALG_3: 11;

        end;

          suppose

           A86: ( the_arity_of o) <> {} ;

          then

          reconsider domar = ( dom ar) as non empty finite set;

          defpred P[ set, set] means ex kn be Function st ex A be strict non-empty finitely-generated MSSubAlgebra of AG st kn = (k . $1) & (for B be strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds (kn . A) = (kn . B)) & ((BA . (ar . $1)) . kn) = (kn . A) & $2 = A;

          

           A87: for n be Element of domar holds ex b be Element of ( MSSub AG) st P[n, b]

          proof

            let n be Element of domar;

            consider g be Function of (the Sorts of PS . (ar . n)), (the Sorts of AG . (ar . n)) such that

             A88: g = (BA . (ar . n)) and

             A89: for x be object st x in (the Sorts of PS . (ar . n)) holds Z[(g . x), x, (ar . n)] by A75, PARTFUN1: 4;

            (k . n) in (the Sorts of PS . (ar /. n)) by MSUALG_6: 2;

            then (k . n) in (the Sorts of PS . (ar . n)) by PARTFUN1:def 6;

            then

            consider s be SortSymbol of SG, f be Element of (( SORTS FF) . s), A be strict non-empty finitely-generated MSSubAlgebra of AG such that s = (ar . n) and

             A90: f = (k . n) and

             A91: for B be strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds (f . A) = (f . B) and

             A92: (g . (k . n)) = (f . A) by A89;

            reconsider b = A as Element of ( MSSub AG) by MSUALG_2:def 19;

            take b, f;

            take A;

            thus f = (k . n) by A90;

            thus for B be strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds (f . A) = (f . B) by A91;

            thus ((BA . (ar . n)) . f) = (f . A) by A88, A90, A92;

            thus thesis;

          end;

          consider KK be Function of domar, ( MSSub AG) such that

           A93: for n be Element of domar holds P[n, (KK . n)] from FUNCT_2:sch 3( A87);

          reconsider KK as ManySortedSet of domar;

          KK is MSAlgebra-Family of domar, SG

          proof

            let n be object;

            assume n in domar;

            then ex kn be Function st ex A be strict non-empty finitely-generated MSSubAlgebra of AG st kn = (k . n) & (for B be strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds (kn . A) = (kn . B)) & ((BA . (ar . n)) . kn) = (kn . A) & (KK . n) = A by A93;

            hence thesis;

          end;

          then

          reconsider KK as MSAlgebra-Family of domar, SG;

          for n be Element of domar holds ex C be strict non-empty finitely-generated MSSubAlgebra of AG st C = (KK . n)

          proof

            let n be Element of domar;

            ex kn be Function st ex A be strict non-empty finitely-generated MSSubAlgebra of AG st kn = (k . n) & (for B be strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds (kn . A) = (kn . B)) & ((BA . (ar . n)) . kn) = (kn . A) & (KK . n) = A by A93;

            hence thesis;

          end;

          then

          consider K be strict non-empty finitely-generated MSSubAlgebra of AG such that

           A94: for n be Element of domar holds (KK . n) is MSSubAlgebra of K by Th25;

          consider MAX be strict non-empty finitely-generated MSSubAlgebra of AG such that

           A95: A is MSSubAlgebra of MAX and

           A96: K is MSSubAlgebra of MAX by Th26;

          MAX in ( MSSub AG) by MSUALG_2:def 19;

          then MAX in CC by A1;

          then

          reconsider iA = MAX as Element of CC;

          

           A97: k in ( Args (o,pr)) by Th18;

          then

           A98: (( commute k) . iA) is Element of ( Args (o,(FF . iA))) by A86, PRALG_3: 20;

          then (( commute k) . iA) in ( Args (o,(FF . iA)));

          then

           A99: (( commute k) . iA) in ( Args (o,MAX)) by A3;

          

           A100: k in ( Funcs (( dom ar),( Funcs (CC,( union the set of all (the Sorts of (FF . i) . m) where i be Element of CC, m be Element of the carrier of SG))))) by A97, PRALG_3: 14;

          then

           A101: ( dom (( commute k) . iA)) = domar by Th3;

          

           A102: for n be object st n in ( dom (( commute k) . iA)) holds ((BA # k) . n) = ((( commute k) . iA) . n)

          proof

            set fs = (( commute k) . iA);

            reconsider fs as Element of ( Args (o,MAX)) by A3, A98;

            let n be object;

            assume

             A103: n in ( dom (( commute k) . iA));

            then

            reconsider arn = (ar . n) as SortSymbol of SG by A101, PARTFUN1: 4;

            n in ( Seg ( len fs)) by A103, FINSEQ_1:def 3;

            then

            reconsider n9 = n as Nat;

            consider kn be Function, Ki be strict non-empty finitely-generated MSSubAlgebra of AG such that

             A104: kn = (k . n) and

             A105: for B be strict non-empty finitely-generated MSSubAlgebra of AG st Ki is MSSubAlgebra of B holds (kn . Ki) = (kn . B) and

             A106: ((BA . arn) . kn) = (kn . Ki) and

             A107: (KK . n) = Ki by A93, A101, A103;

            

             A108: Ki is MSSubAlgebra of K by A94, A101, A103, A107;

            ( dom k) = domar by A100, FUNCT_2: 92;

            

            hence ((BA # k) . n) = ((BA . (ar /. n9)) . (k . n)) by A101, A103, MSUALG_3:def 6

            .= (kn . (KK . n)) by A101, A103, A104, A106, A107, PARTFUN1:def 6

            .= (kn . iA) by A96, A105, A107, A108, MSUALG_2: 6

            .= ((( commute k) . iA) . n) by A97, A101, A103, A104, PRALG_3: 21;

          end;

          reconsider ff1 = (( Den (o,pr)) . k) as Function by Th20;

          

           A109: ( dom (BA # k)) = domar by MSUALG_6: 2;

          

          thus ((BA . ( the_result_sort_of o)) . (( Den (o,PS)) . k)) = (f . MAX) by A76, A79, A80, A95

          .= (ff1 . MAX) by A78, Th19

          .= (( Den (o,(FF . iA))) . (( commute k) . iA)) by A86, A97, PRALG_3: 22

          .= (( Den (o,MAX)) . (( commute k) . iA)) by A3

          .= (( Den (o,AG)) . (( commute k) . iA)) by A99, Th19

          .= (( Den (o,AG)) . (BA # k)) by A100, A109, A102, Th3, FUNCT_1: 2;

        end;

      end;

      let i be set;

      assume i in I;

      then

      reconsider s = i as SortSymbol of SG;

      consider ff be object such that

       A110: ff in (the Sorts of PS . s) by XBOOLE_0:def 1;

      ( rng (BA . s)) c= (the Sorts of AG . s);

      hence ( rng (BA . i)) c= (the Sorts of AG . i);

      let y be object such that

       A111: y in (the Sorts of AG . i);

      

       A112: (( SORTS FF) . s) = ( product ( Carrier (FF,s))) by PRALG_2:def 10;

      then ff in ( product ( Carrier (FF,s))) by A4, A40, A110;

      then

      consider aa be Function such that ff = aa and

       A113: ( dom aa) = ( dom ( Carrier (FF,s))) and

       A114: for x be object st x in ( dom ( Carrier (FF,s))) holds (aa . x) in (( Carrier (FF,s)) . x) by CARD_3:def 5;

      defpred KK[ object] means ex Axx be MSSubAlgebra of AG st Axx = $1 & y in (the Sorts of Axx . s);

      consider WW be set such that

       A115: for a be object holds a in WW iff a in CC & KK[a] from XBOOLE_0:sch 1;

      set XX = (aa +* (WW --> y));

      

       A116: ( dom (WW --> y)) = WW;

      

       A117: for xx be Element of CC st KK[xx] holds (XX . xx) = y

      proof

        let xx be Element of CC;

        assume KK[xx];

        then

         A118: xx in WW by A115;

        

        hence (XX . xx) = ((WW --> y) . xx) by A116, FUNCT_4: 13

        .= y by A118, FUNCOP_1: 7;

      end;

      

       A119: ( dom ( Carrier (FF,s))) = CC by PARTFUN1:def 2;

      

       A120: for x be object st x in ( dom ( Carrier (FF,s))) holds (XX . x) in (( Carrier (FF,s)) . x)

      proof

        let x be object;

        assume

         A121: x in ( dom ( Carrier (FF,s)));

        then

        consider C be Element of ( MSSub AG) such that

         A122: x = C and

         A123: ex R be strict non-empty finitely-generated MSSubAlgebra of AG st R = C by A1, A119;

        consider R be strict non-empty finitely-generated MSSubAlgebra of AG such that

         A124: R = C by A123;

        

         A125: R in CC by A1, A124;

        then

         A126: (ex U0 be MSAlgebra over SG st U0 = (FF . R) & (( Carrier (FF,s)) . R) = (the Sorts of U0 . s)) & (FF . R) = R by A3, PRALG_2:def 9;

        per cases ;

          suppose KK[x];

          hence thesis by A117, A122, A124, A125, A126;

        end;

          suppose not KK[x];

          then not x in WW by A115;

          then (XX . x) = (aa . x) by A116, FUNCT_4: 11;

          hence thesis by A114, A121;

        end;

      end;

      

       A127: WW c= CC by A115;

      set L = the non-empty finite-yielding MSSubset of AG;

      

       A128: ( dom (BA . s)) = (the Sorts of PS . s) by FUNCT_2:def 1;

      set SY = ( {s} --> {y});

      ( dom (L +* SY)) = (( dom L) \/ ( dom SY)) by FUNCT_4:def 1

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

      .= (I \/ {s})

      .= I by ZFMISC_1: 40;

      then

      reconsider Y = (L +* SY) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      

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

      ( dom SY) = {s};

      

      then

       A130: (Y . s) = (SY . s) by A129, FUNCT_4: 13

      .= {y} by A129, FUNCOP_1: 7;

       A131:

      now

        let k be set;

        assume that k in I and

         A132: k <> s;

         not k in ( dom SY) by A132, TARSKI:def 1;

        hence (Y . k) = (L . k) by FUNCT_4: 11;

      end;

      Y is ManySortedSubset of the Sorts of AG

      proof

        let j be object such that

         A133: j in I;

        let x be object such that

         A134: x in (Y . j);

        per cases ;

          suppose

           A135: j <> s;

          L c= the Sorts of AG by PBOOLE:def 18;

          then

           A136: (L . j) c= (the Sorts of AG . j) by A133;

          x in (L . j) by A131, A133, A134, A135;

          hence thesis by A136;

        end;

          suppose j = s;

          hence thesis by A111, A130, A134, TARSKI:def 1;

        end;

      end;

      then

      reconsider Y as MSSubset of AG;

      Y is non-empty

      proof

        let j be object such that

         A137: j in I;

        per cases ;

          suppose j <> s;

          then (Y . j) = (L . j) by A131, A137;

          hence thesis by A137;

        end;

          suppose j = s;

          hence thesis by A130;

        end;

      end;

      then

      reconsider Y as non-empty MSSubset of AG;

      Y is finite-yielding

      proof

        let j be object such that

         A138: j in I;

        per cases ;

          suppose j <> s;

          then (Y . j) = (L . j) by A131, A138;

          hence thesis;

        end;

          suppose j = s;

          hence thesis by A130;

        end;

      end;

      then

      reconsider Y as non-empty finite-yielding MSSubset of AG;

      Y is MSSubset of ( GenMSAlg Y) by MSUALG_2:def 17;

      then Y c= the Sorts of ( GenMSAlg Y) by PBOOLE:def 18;

      then

       A139: (Y . s) c= (the Sorts of ( GenMSAlg Y) . s);

      ( dom XX) = (( dom aa) \/ ( dom (WW --> y))) by FUNCT_4:def 1

      .= (CC \/ ( dom (WW --> y))) by A113, PARTFUN1:def 2

      .= (CC \/ WW)

      .= CC by A127, XBOOLE_1: 12;

      then

      reconsider XX as Element of (( SORTS FF) . s) by A112, A119, A120, CARD_3: 9;

      consider h be Function of (the Sorts of PS . s), (the Sorts of AG . s) such that

       A140: h = (BA . s) and

       A141: for x be object st x in (the Sorts of PS . s) holds Z[(h . x), x, s] by A75;

      

       A142: y in (Y . s) by A130, TARSKI:def 1;

      then

       A143: y in (the Sorts of ( GenMSAlg Y) . s) by A139;

       T[s, XX]

      proof

        take s;

        take XX;

        take TT = ( GenMSAlg Y);

        thus s = s;

        thus XX = XX;

        let B be strict non-empty finitely-generated MSSubAlgebra of AG;

        assume TT is MSSubAlgebra of B;

        then the Sorts of TT is ManySortedSubset of the Sorts of B by MSUALG_2:def 9;

        then the Sorts of TT c= the Sorts of B by PBOOLE:def 18;

        then

         A144: (the Sorts of TT . s) c= (the Sorts of B . s);

        

         A145: B in CC by A2;

        TT in CC by A2;

        

        hence (XX . TT) = y by A139, A142, A117

        .= (XX . B) by A143, A117, A145, A144;

      end;

      then

       A146: XX in (SOR . s) by A4;

      then Z[(h . XX), XX, s] by A40, A141;

      then

      consider t be SortSymbol of SG, f be Element of (( SORTS FF) . s), A be strict non-empty finitely-generated MSSubAlgebra of AG such that s = t and

       A147: (f = XX & for B be strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds (f . A) = (f . B)) & (h . XX) = (f . A);

      consider MAX be strict non-empty finitely-generated MSSubAlgebra of AG such that

       A148: A is MSSubAlgebra of MAX and

       A149: ( GenMSAlg Y) is MSSubAlgebra of MAX by Th26;

      

       A150: MAX in CC by A2;

      the Sorts of ( GenMSAlg Y) is ManySortedSubset of the Sorts of MAX by A149, MSUALG_2:def 9;

      then the Sorts of ( GenMSAlg Y) c= the Sorts of MAX by PBOOLE:def 18;

      then

       A151: (the Sorts of ( GenMSAlg Y) . s) c= (the Sorts of MAX . s);

      (h . XX) = (XX . MAX) by A147, A148

      .= y by A143, A117, A151, A150;

      hence thesis by A40, A128, A140, A146, FUNCT_1:def 3;

    end;

    theorem :: EQUATION:28

    for U0 be feasible free MSAlgebra over S, A be free GeneratorSet of U0 holds for Z be MSSubset of U0 st Z c= A & ( GenMSAlg Z) is feasible holds ( GenMSAlg Z) is free

    proof

      let U0 be feasible free MSAlgebra over S, A be free GeneratorSet of U0, Z be MSSubset of U0 such that

       A1: Z c= A and

       A2: ( GenMSAlg Z) is feasible;

      reconsider Z1 = Z as MSSubset of ( GenMSAlg Z) by MSUALG_2:def 17;

      the Sorts of ( GenMSAlg Z1) = the Sorts of ( GenMSAlg Z) by EXTENS_1: 18;

      then

      reconsider z = Z as GeneratorSet of ( GenMSAlg Z) by MSAFREE:def 4;

      reconsider z1 = z as ManySortedSubset of A by A1, PBOOLE:def 18;

      take z;

      z is free

      proof

        reconsider D = the Sorts of ( GenMSAlg Z) as MSSubset of U0 by MSUALG_2:def 9;

        let U1 be non-empty MSAlgebra over S, g be ManySortedFunction of z, the Sorts of U1;

        consider G be ManySortedFunction of A, the Sorts of U1 such that

         A3: (G || z1) = g by Th6;

        consider h be ManySortedFunction of U0, U1 such that

         A4: h is_homomorphism (U0,U1) and

         A5: (h || A) = G by MSAFREE:def 5;

        reconsider H = (h || D) as ManySortedFunction of ( GenMSAlg Z), U1;

        take H;

        thus H is_homomorphism (( GenMSAlg Z),U1) by A2, A4, Th22;

        

        thus g = (h || Z) by A3, A5, Th5

        .= (H || z) by Th5;

      end;

      hence thesis;

    end;

    begin

    definition

      let S be non empty non void ManySortedSign;

      :: EQUATION:def3

      func TermAlg S -> MSAlgebra over S equals ( FreeMSA (the carrier of S --> NAT ));

      correctness ;

    end

    registration

      let S be non empty non void ManySortedSign;

      cluster ( TermAlg S) -> strict non-empty free;

      coherence ;

    end

    definition

      let S be non empty non void ManySortedSign;

      :: EQUATION:def4

      func Equations S -> ManySortedSet of the carrier of S equals [|the Sorts of ( TermAlg S), the Sorts of ( TermAlg S)|];

      correctness ;

    end

    registration

      let S be non empty non void ManySortedSign;

      cluster ( Equations S) -> non-empty;

      coherence ;

    end

    definition

      let S be non empty non void ManySortedSign;

      mode EqualSet of S is ManySortedSubset of ( Equations S);

    end

    reserve s for SortSymbol of S;

    reserve e for Element of (( Equations S) . s);

    reserve E for EqualSet of S;

    notation

      let S be non empty non void ManySortedSign, s be SortSymbol of S, x,y be Element of (the Sorts of ( TermAlg S) . s);

      synonym x '=' y for [x,y];

    end

    definition

      let S be non empty non void ManySortedSign, s be SortSymbol of S, x,y be Element of (the Sorts of ( TermAlg S) . s);

      :: original: '='

      redefine

      func x '=' y -> Element of (( Equations S) . s) ;

      coherence

      proof

         [x, y] in [:(the Sorts of ( TermAlg S) . s), (the Sorts of ( TermAlg S) . s):] by ZFMISC_1: 87;

        hence thesis by PBOOLE:def 16;

      end;

    end

    theorem :: EQUATION:29

    

     Th29: (e `1 ) in (the Sorts of ( TermAlg S) . s)

    proof

      set T = the Sorts of ( TermAlg S);

      e is Element of [:(T . s), (T . s):] by PBOOLE:def 16;

      hence thesis by MCART_1: 10;

    end;

    theorem :: EQUATION:30

    

     Th30: (e `2 ) in (the Sorts of ( TermAlg S) . s)

    proof

      set T = the Sorts of ( TermAlg S);

      e is Element of [:(T . s), (T . s):] by PBOOLE:def 16;

      hence thesis by MCART_1: 10;

    end;

    definition

      let S be non empty non void ManySortedSign, A be MSAlgebra over S, s be SortSymbol of S, e be Element of (( Equations S) . s);

      :: EQUATION:def5

      pred A |= e means for h be ManySortedFunction of ( TermAlg S), A st h is_homomorphism (( TermAlg S),A) holds ((h . s) . (e `1 )) = ((h . s) . (e `2 ));

    end

    definition

      let S be non empty non void ManySortedSign, A be MSAlgebra over S, E be EqualSet of S;

      :: EQUATION:def6

      pred A |= E means for s be SortSymbol of S holds for e be Element of (( Equations S) . s) st e in (E . s) holds A |= e;

    end

    theorem :: EQUATION:31

    

     Th31: for U2 be strict non-empty MSSubAlgebra of U0 st U0 |= e holds U2 |= e

    proof

      let U2 be strict non-empty MSSubAlgebra of U0 such that

       A1: U0 |= e;

      let h be ManySortedFunction of ( TermAlg S), U2 such that

       A2: h is_homomorphism (( TermAlg S),U2);

      

       A3: the Sorts of ( TermAlg S) is_transformable_to the Sorts of U2;

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

      then

      reconsider f1 = h as ManySortedFunction of ( TermAlg S), U0 by A3, EXTENS_1: 5;

      f1 is_homomorphism (( TermAlg S),U0) by A2, MSUALG_9: 15;

      hence thesis by A1;

    end;

    theorem :: EQUATION:32

    for U2 be strict non-empty MSSubAlgebra of U0 st U0 |= E holds U2 |= E by Th31;

    theorem :: EQUATION:33

    

     Th33: (U0,U1) are_isomorphic & U0 |= e implies U1 |= e

    proof

      assume that

       A1: (U0,U1) are_isomorphic and

       A2: U0 |= e;

      consider F be ManySortedFunction of U0, U1 such that

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

      consider G be ManySortedFunction of U1, U0 such that

       A4: G = (F "" );

      F is "1-1" & F is "onto" by A3, MSUALG_3: 13;

      then

       A5: (G . s) = ((F . s) " ) by A4, MSUALG_3:def 4;

      F is "onto" by A3, MSUALG_3: 13;

      then

       A6: ( rng (F . s)) = (the Sorts of U1 . s);

      let h1 be ManySortedFunction of ( TermAlg S), U1 such that

       A7: h1 is_homomorphism (( TermAlg S),U1);

      set F1 = (G ** h1);

      G is_isomorphism (U1,U0) by A3, A4, MSUALG_3: 14;

      then G is_homomorphism (U1,U0) by MSUALG_3: 13;

      then

       A8: F1 is_homomorphism (( TermAlg S),U0) by A7, MSUALG_3: 10;

      F is "1-1" by A3, MSUALG_3: 13;

      then

       A9: (F . s) is one-to-one by MSUALG_3: 1;

      (F1 . s) = ((G . s) * (h1 . s)) by MSUALG_3: 2;

      

      then

       A10: ((F . s) * (F1 . s)) = (((F . s) * (G . s)) * (h1 . s)) by RELAT_1: 36

      .= (( id (the Sorts of U1 . s)) * (h1 . s)) by A5, A6, A9, FUNCT_2: 29

      .= (h1 . s) by FUNCT_2: 17;

      

       A11: ( dom (F1 . s)) = (the Sorts of ( TermAlg S) . s) by FUNCT_2:def 1;

      

      hence ((h1 . s) . (e `1 )) = ((F . s) . ((F1 . s) . (e `1 ))) by A10, Th29, FUNCT_1: 13

      .= ((F . s) . ((F1 . s) . (e `2 ))) by A2, A8

      .= ((h1 . s) . (e `2 )) by A10, A11, Th30, FUNCT_1: 13;

    end;

    theorem :: EQUATION:34

    (U0,U1) are_isomorphic & U0 |= E implies U1 |= E by Th33;

    theorem :: EQUATION:35

    

     Th35: for R be MSCongruence of U0 st U0 |= e holds ( QuotMSAlg (U0,R)) |= e

    proof

      let R be MSCongruence of U0 such that

       A1: U0 |= e;

      set n = (( MSNat_Hom (U0,R)) . s);

      let h be ManySortedFunction of ( TermAlg S), ( QuotMSAlg (U0,R));

      assume h is_homomorphism (( TermAlg S),( QuotMSAlg (U0,R)));

      then

      consider h0 be ManySortedFunction of ( TermAlg S), U0 such that

       A2: h0 is_homomorphism (( TermAlg S),U0) and

       A3: h = (( MSNat_Hom (U0,R)) ** h0) by Th24, MSUALG_4: 3;

      

       A4: ( dom (h0 . s)) = (the Sorts of ( TermAlg S) . s) by FUNCT_2:def 1;

      

      thus ((h . s) . (e `1 )) = ((n * (h0 . s)) . (e `1 )) by A3, MSUALG_3: 2

      .= (n . ((h0 . s) . (e `1 ))) by A4, Th29, FUNCT_1: 13

      .= (n . ((h0 . s) . (e `2 ))) by A1, A2

      .= ((n * (h0 . s)) . (e `2 )) by A4, Th30, FUNCT_1: 13

      .= ((h . s) . (e `2 )) by A3, MSUALG_3: 2;

    end;

    theorem :: EQUATION:36

    for R be MSCongruence of U0 st U0 |= E holds ( QuotMSAlg (U0,R)) |= E by Th35;

    

     Lm1: for I be non empty set, A be MSAlgebra-Family of I, S st for i be Element of I holds (A . i) |= e holds ( product A) |= e

    proof

      reconsider e2 = (e `2 ) as Element of (the Sorts of ( TermAlg S) . s) by Th30;

      reconsider e1 = (e `1 ) as Element of (the Sorts of ( TermAlg S) . s) by Th29;

      let I be non empty set, A be MSAlgebra-Family of I, S such that

       A1: for i be Element of I holds (A . i) |= e;

      let h be ManySortedFunction of ( TermAlg S), ( product A) such that

       A2: h is_homomorphism (( TermAlg S),( product A));

      

       A3: ( dom (h . s)) = (the Sorts of ( TermAlg S) . s) by FUNCT_2:def 1;

       A4:

      now

        let i be Element of I;

        set Z = (( proj (A,i)) ** h);

        

         A5: (A . i) |= e by A1;

        ( proj (A,i)) is_homomorphism (( product A),(A . i)) by PRALG_3: 24;

        then

         A6: (( proj (A,i)) ** h) is_homomorphism (( TermAlg S),(A . i)) by A2, MSUALG_3: 10;

        

        thus (( proj (( Carrier (A,s)),i)) . ((h . s) . e1)) = ((( proj (A,i)) . s) . ((h . s) . e1)) by PRALG_3:def 2

        .= (((( proj (A,i)) . s) * (h . s)) . e1) by A3, FUNCT_1: 13

        .= ((Z . s) . e1) by MSUALG_3: 2

        .= ((Z . s) . e2) by A5, A6

        .= (((( proj (A,i)) . s) * (h . s)) . e2) by MSUALG_3: 2

        .= ((( proj (A,i)) . s) . ((h . s) . e2)) by A3, FUNCT_1: 13

        .= (( proj (( Carrier (A,s)),i)) . ((h . s) . e2)) by PRALG_3:def 2;

      end;

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

      hence thesis by A4, MSUALG_9: 14;

    end;

    theorem :: EQUATION:37

    

     Th37: for F be MSAlgebra-Family of I, S st (for i be set st i in I holds ex A be MSAlgebra over S st A = (F . i) & A |= e) holds ( product F) |= e

    proof

      let F be MSAlgebra-Family of I, S such that

       A1: for i be set st i in I holds ex A be MSAlgebra over S st A = (F . i) & A |= e;

      per cases ;

        suppose I = {} ;

        then

        reconsider J = I as empty set;

        reconsider FJ = F as MSAlgebra-Family of J, S;

        thus ( product F) |= e

        proof

          let h be ManySortedFunction of ( TermAlg S), ( product F) such that h is_homomorphism (( TermAlg S),( product F));

          

           A2: (the Sorts of ( product FJ) . s) = ( product ( Carrier (FJ,s))) by PRALG_2:def 10

          .= { {} } by CARD_3: 10;

          

           A3: ((h . s) . (e `2 )) in (the Sorts of ( product FJ) . s) by Th30, FUNCT_2: 5;

          ((h . s) . (e `1 )) in (the Sorts of ( product FJ) . s) by Th29, FUNCT_2: 5;

          

          hence ((h . s) . (e `1 )) = {} by A2, TARSKI:def 1

          .= ((h . s) . (e `2 )) by A2, A3, TARSKI:def 1;

        end;

      end;

        suppose I <> {} ;

        then

        reconsider J = I as non empty set;

        reconsider F1 = F as MSAlgebra-Family of J, S;

        now

          let i be Element of J;

          ex A be MSAlgebra over S st A = (F1 . i) & A |= e by A1;

          hence (F1 . i) |= e;

        end;

        hence thesis by Lm1;

      end;

    end;

    theorem :: EQUATION:38

    for F be MSAlgebra-Family of I, S st (for i be set st i in I holds ex A be MSAlgebra over S st A = (F . i) & A |= E) holds ( product F) |= E

    proof

      let F be MSAlgebra-Family of I, S such that

       A1: for i be set st i in I holds ex A be MSAlgebra over S st A = (F . i) & A |= E;

      let s be SortSymbol of S, e be Element of (( Equations S) . s) such that

       A2: e in (E . s);

      now

        let i be set;

        assume i in I;

        then

        consider A be MSAlgebra over S such that

         A3: A = (F . i) & A |= E by A1;

        take A;

        thus A = (F . i) & A |= e by A2, A3;

      end;

      hence thesis by Th37;

    end;