birkhoff.miz



    begin

    definition

      let S be non empty non void ManySortedSign, X be non-empty ManySortedSet of the carrier of S, A be non-empty MSAlgebra over S, F be ManySortedFunction of X, the Sorts of A;

      :: BIRKHOFF:def1

      func F -hash -> ManySortedFunction of ( FreeMSA X), A means

      : Def1: it is_homomorphism (( FreeMSA X),A) & (it || ( FreeGen X)) = (F ** ( Reverse X));

      existence by MSAFREE:def 5;

      uniqueness by EXTENS_1: 14;

    end

    theorem :: BIRKHOFF:1

    

     Th1: for S be non empty non void ManySortedSign holds for A be non-empty MSAlgebra over S holds for X be non-empty ManySortedSet of the carrier of S holds for F be ManySortedFunction of X, the Sorts of A holds ( rngs F) c= ( rngs (F -hash ))

    proof

      let S be non empty non void ManySortedSign, A be non-empty MSAlgebra over S, X be non-empty ManySortedSet of the carrier of S, F be ManySortedFunction of X, the Sorts of A;

      set R = ( Reverse X);

      let i be object;

      assume i in the carrier of S;

      then

      reconsider s = i as SortSymbol of S;

      let y be object;

      

       A1: ( dom (R . s)) = (( FreeGen X) . s) by FUNCT_2:def 1;

      ( FreeGen X) c= the Sorts of ( FreeMSA X) by PBOOLE:def 18;

      then

       A2: (( FreeGen X) . s) c= (the Sorts of ( FreeMSA X) . s);

      assume y in (( rngs F) . i);

      then y in ( rng (F . s)) by MSSUBFAM: 13;

      then

      consider x be object such that

       A3: x in ( dom (F . s)) and

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

      ( rngs R) = X by EXTENS_1: 10;

      then R is "onto" by EXTENS_1: 9;

      then ( rng (R . s)) = (X . s) by MSUALG_3:def 3;

      then

      consider a be object such that

       A5: a in ( dom (R . s)) and

       A6: x = ((R . s) . a) by A3, FUNCT_1:def 3;

      

       A7: ( dom ((F -hash ) . s)) = (the Sorts of ( FreeMSA X) . s) by FUNCT_2:def 1;

      y = (((F . s) * (R . s)) . a) by A4, A5, A6, FUNCT_1: 13

      .= (((F ** R) . s) . a) by MSUALG_3: 2

      .= ((((F -hash ) || ( FreeGen X)) . s) . a) by Def1

      .= ((((F -hash ) . s) | (( FreeGen X) . s)) . a) by MSAFREE:def 1

      .= (((F -hash ) . s) . a) by A5, FUNCT_1: 49;

      then y in ( rng ((F -hash ) . s)) by A5, A1, A7, A2, FUNCT_1:def 3;

      hence thesis by MSSUBFAM: 13;

    end;

    scheme :: BIRKHOFF:sch1

    ExFreeAlg1 { S() -> non empty non void ManySortedSign , X() -> non-empty MSAlgebra over S() , P[ set] } :

ex A be strict non-empty MSAlgebra over S(), F be ManySortedFunction of X(), A st P[A] & F is_epimorphism (X(),A) & for B be non-empty MSAlgebra over S() holds for G be ManySortedFunction of X(), B st G is_homomorphism (X(),B) & P[B] holds ex H be ManySortedFunction of A, B st H is_homomorphism (A,B) & (H ** F) = G & for K be ManySortedFunction of A, B st (K ** F) = G holds H = K

      provided

       A1: for A,B be non-empty MSAlgebra over S() st (A,B) are_isomorphic & P[A] holds P[B]

       and

       A2: for A be non-empty MSAlgebra over S() holds for B be strict non-empty MSSubAlgebra of A st P[A] holds P[B]

       and

       A3: for I be set, 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) & P[A]) holds P[( product F)];

      set EMF = the MSAlgebra-Family of {} , S();

      set CC = { C where C be Element of ( CongrLatt X()) : ex R be MSCongruence of X() st R = C & P[( QuotMSAlg (X(),R))] };

      set SF = the Sorts of X(), I = the carrier of S();

      consider Xi be ManySortedSet of I such that

       A4: {Xi} = (I --> { {} }) by MSUALG_9: 5;

      now

        let i be object;

        assume i in I;

        then

        reconsider s = i as SortSymbol of S();

        

        thus (the Sorts of ( product EMF) . i) = ( product ( Carrier (EMF,s))) by PRALG_2:def 10

        .= { {} } by CARD_3: 10, PRALG_2:def 9

        .= ((I --> { {} }) . s)

        .= ( {Xi} . i) by A4;

      end;

      then

       A5: the Sorts of ( product EMF) = {Xi};

      reconsider R = [|SF, SF|] as MSCongruence of X() by MSUALG_5: 18;

       [|SF, SF|] is MSCongruence of X() by MSUALG_5: 18;

      then

       A6: [|SF, SF|] is Element of ( CongrLatt X()) by MSUALG_5:def 6;

      the Sorts of ( QuotMSAlg (X(),R)) = {SF} by MSUALG_9: 29;

      then

       A7: (( QuotMSAlg (X(),R)),( Trivial_Algebra S())) are_isomorphic by MSUALG_9: 26;

      for i be set st i in {} holds ex A be MSAlgebra over S() st A = (EMF . i) & P[A];

      then P[( product EMF)] by A3;

      then P[( Trivial_Algebra S())] by A1, A5, MSUALG_9: 26;

      then P[( QuotMSAlg (X(),R))] by A1, A7, MSUALG_3: 17;

      then

       A8: [|SF, SF|] in CC by A6;

      defpred P[ object, object] means ex R be MSCongruence of X() st R = $1 & $2 = ( QuotMSAlg (X(),R));

      defpred P1[ set] means ex R be MSCongruence of X() st R = $1 & P[( QuotMSAlg (X(),R))];

       A9:

      now

        let q be object;

        assume q in CC;

        then ex C be Element of ( CongrLatt X()) st q = C & ex R be MSCongruence of X() st R = C & P[( QuotMSAlg (X(),R))];

        hence q is MSCongruence of X();

      end;

      

       A10: CC c= the carrier of ( EqRelLatt SF)

      proof

        let q be object;

        assume q in CC;

        then q is Equivalence_Relation of SF by A9;

        hence thesis by MSUALG_5:def 5;

      end;

      then

      reconsider CC as non empty SubsetFamily of [|SF, SF|] by A8, MSUALG_7: 5;

      set R0 = ( meet |:CC:|);

      

       A11: R0 is MSEquivalence_Relation-like ManySortedRelation of SF by A10, MSUALG_7: 8;

      reconsider R0 as ManySortedRelation of X() by A10, MSUALG_7: 8;

      R0 is MSEquivalence-like by A11;

      then

      reconsider R0 as MSEquivalence-like ManySortedRelation of X();

      { C where C be Element of ( CongrLatt X()) : P1[C] } is Subset of ( CongrLatt X()) from DOMAIN_1:sch 7;

      then

      reconsider R0 as MSCongruence of X() by MSUALG_9: 28;

      take A = ( QuotMSAlg (X(),R0));

      reconsider F = ( MSNat_Hom (X(),R0)) as ManySortedFunction of X(), A;

      take F;

       A12:

      now

        let c be object;

        assume c in CC;

        then

        reconsider cc = c as MSCongruence of X() by A9;

        reconsider w = ( QuotMSAlg (X(),cc)) as object;

        take w;

        thus P[c, w];

      end;

      consider FF be ManySortedSet of CC such that

       A13: for c be object st c in CC holds P[c, (FF . c)] from PBOOLE:sch 3( A12);

      FF is MSAlgebra-Family of CC, S()

      proof

        let c be object;

        assume c in CC;

        then ex R be MSCongruence of X() st R = c & (FF . c) = ( QuotMSAlg (X(),R)) by A13;

        hence thesis;

      end;

      then

      reconsider FF as MSAlgebra-Family of CC, S();

      defpred P[ Element of CC, object] means ex F1 be ManySortedFunction of X(), (FF . $1) st F1 = $2 & F1 is_homomorphism (X(),(FF . $1)) & ex R be MSCongruence of X() st $1 = R & F1 = ( MSNat_Hom (X(),R));

      

       A14: for c be Element of CC holds ex j be object st P[c, j]

      proof

        let c be Element of CC;

        consider R be MSCongruence of X() such that

         A15: R = c and

         A16: (FF . c) = ( QuotMSAlg (X(),R)) by A13;

        set j = ( MSNat_Hom (X(),R));

        reconsider F1 = j as ManySortedFunction of X(), (FF . c) by A16;

        take j;

        take F1;

        thus F1 = j;

        ( MSNat_Hom (X(),R)) is_epimorphism (X(),( QuotMSAlg (X(),R))) by MSUALG_4: 3;

        hence F1 is_homomorphism (X(),(FF . c)) by A16, MSUALG_3:def 8;

        take R;

        thus thesis by A15;

      end;

      consider FofI1 be ManySortedSet of CC such that

       A17: for c be Element of CC holds P[c, (FofI1 . c)] from PBOOLE:sch 6( A14);

      

       A18: for c be Element of CC holds ex F1 be ManySortedFunction of X(), (FF . c) st F1 = (FofI1 . c) & F1 is_homomorphism (X(),(FF . c))

      proof

        let c be Element of CC;

        consider F1 be ManySortedFunction of X(), (FF . c) such that

         A19: F1 = (FofI1 . c) and

         A20: F1 is_homomorphism (X(),(FF . c)) and ex R be MSCongruence of X() st c = R & F1 = ( MSNat_Hom (X(),R)) by A17;

        take F1;

        thus thesis by A19, A20;

      end;

      FofI1 is Function-yielding

      proof

        let c be object;

        assume c in ( dom FofI1);

        then

        reconsider cc = c as Element of CC;

        ex F1 be ManySortedFunction of X(), (FF . cc) st F1 = (FofI1 . cc) & F1 is_homomorphism (X(),(FF . cc)) by A18;

        hence thesis;

      end;

      then

      reconsider FofI1 as ManySortedFunction of CC;

      consider H be ManySortedFunction of X(), ( product FF) such that

       A21: H is_homomorphism (X(),( product FF)) and

       A22: for c be Element of CC holds (( proj (FF,c)) ** H) = (FofI1 . c) by A18, PRALG_3: 29;

      now

        let i be object;

        assume i in I;

        then

        reconsider s = i as SortSymbol of S();

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

         A23: Q = ( |:CC:| . s) and

         A24: (( meet |:CC:|) . s) = ( Intersect Q) by MSSUBFAM:def 1;

        

         A25: ( |:CC:| . s) = { (t . s) where t be Element of ( Bool [|SF, SF|]) : t in CC } by CLOSURE2: 14;

        (( MSCng H) . s) = (R0 . s)

        proof

          let a,b be object;

          hereby

            assume

             A26: [a, b] in (( MSCng H) . s);

            then

             A27: a in (SF . s) by ZFMISC_1: 87;

            

             A28: b in (SF . s) by A26, ZFMISC_1: 87;

            

             A29: [a, b] in ( MSCng (H,s)) by A21, A26, MSUALG_4:def 18;

            

             A30: for Y be set st Y in Q holds [a, b] in Y

            proof

              let Y be set;

              assume Y in Q;

              then

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

               A31: Y = (t . s) and

               A32: t in CC by A23, A25;

              reconsider t1 = t as Element of CC by A32;

              consider F1 be ManySortedFunction of X(), (FF . t1) such that

               A33: F1 = (FofI1 . t1) and F1 is_homomorphism (X(),(FF . t1)) and

               A34: ex R be MSCongruence of X() st t1 = R & F1 = ( MSNat_Hom (X(),R)) by A17;

              ((F1 . s) . a) = (((( proj (FF,t1)) ** H) . s) . a) by A22, A33

              .= (((( proj (FF,t1)) . s) * (H . s)) . a) by MSUALG_3: 2

              .= ((( proj (FF,t1)) . s) . ((H . s) . a)) by A27, FUNCT_2: 15

              .= ((( proj (FF,t1)) . s) . ((H . s) . b)) by A27, A28, A29, MSUALG_4:def 17

              .= (((( proj (FF,t1)) . s) * (H . s)) . b) by A28, FUNCT_2: 15

              .= (((( proj (FF,t1)) ** H) . s) . b) by MSUALG_3: 2

              .= ((F1 . s) . b) by A22, A33;

              hence thesis by A27, A28, A31, A34, MSUALG_9: 33;

            end;

             [a, b] in [:(SF . s), (SF . s):] by A26;

            then [a, b] in ( [|SF, SF|] . s) by PBOOLE:def 16;

            hence [a, b] in (R0 . s) by A24, A30, SETFAM_1: 43;

          end;

          assume

           A35: [a, b] in (R0 . s);

          then

           A36: a in (SF . s) by ZFMISC_1: 87;

          

           A37: b in (SF . s) by A35, ZFMISC_1: 87;

          

           A38: for c be Element of CC holds (( proj (( Carrier (FF,s)),c)) . ((H . s) . a)) = (( proj (( Carrier (FF,s)),c)) . ((H . s) . b))

          proof

            let c be Element of CC;

            reconsider t1 = c as MSCongruence of X() by A9;

            consider F1 be ManySortedFunction of X(), (FF . c) such that

             A39: F1 = (FofI1 . c) and F1 is_homomorphism (X(),(FF . c)) and

             A40: ex R be MSCongruence of X() st c = R & F1 = ( MSNat_Hom (X(),R)) by A17;

            t1 is Element of ( Bool [|SF, SF|]) by CLOSURE2:def 1;

            then (t1 . s) in ( |:CC:| . s) by A25;

            then

             A41: [a, b] in (t1 . s) by A23, A24, A35, SETFAM_1: 43;

            

            thus (( proj (( Carrier (FF,s)),c)) . ((H . s) . a)) = ((( proj (FF,c)) . s) . ((H . s) . a)) by PRALG_3:def 2

            .= (((( proj (FF,c)) . s) * (H . s)) . a) by A36, FUNCT_2: 15

            .= (((( proj (FF,c)) ** H) . s) . a) by MSUALG_3: 2

            .= ((F1 . s) . a) by A22, A39

            .= ((F1 . s) . b) by A36, A37, A41, A40, MSUALG_9: 33

            .= (((( proj (FF,c)) ** H) . s) . b) by A22, A39

            .= (((( proj (FF,c)) . s) * (H . s)) . b) by MSUALG_3: 2

            .= ((( proj (FF,c)) . s) . ((H . s) . b)) by A37, FUNCT_2: 15

            .= (( proj (( Carrier (FF,s)),c)) . ((H . s) . b)) by PRALG_3:def 2;

          end;

          ((H . s) . b) in (the Sorts of ( product FF) . s) by A37, FUNCT_2: 5;

          then

           A42: ((H . s) . b) in ( product ( Carrier (FF,s))) by PRALG_2:def 10;

          ((H . s) . a) in (the Sorts of ( product FF) . s) by A36, FUNCT_2: 5;

          then ((H . s) . a) in ( product ( Carrier (FF,s))) by PRALG_2:def 10;

          then ((H . s) . a) = ((H . s) . b) by A42, A38, MSUALG_9: 14;

          then [a, b] in ( MSCng (H,s)) by A36, A37, MSUALG_4:def 17;

          hence thesis by A21, MSUALG_4:def 18;

        end;

        hence (( MSCng H) . i) = (R0 . i);

      end;

      then

       A43: ( MSCng H) = R0;

      (( QuotMSAlg (X(),( MSCng H))),( Image ( MSHomQuot H))) are_isomorphic by A21, MSUALG_4: 4, MSUALG_9: 16;

      then

      consider XX be strict non-empty MSSubAlgebra of ( product FF) such that

       A44: (A,XX) are_isomorphic by A43;

      for cc be set st cc in CC holds ex A be MSAlgebra over S() st A = (FF . cc) & P[A]

      proof

        let cc be set;

        assume

         A45: cc in CC;

        then

        reconsider c = cc as Element of CC;

        take (FF . c);

        

         A46: ex C be Element of ( CongrLatt X()) st cc = C & ex R be MSCongruence of X() st R = C & P[( QuotMSAlg (X(),R))] by A45;

        ex R be MSCongruence of X() st R = cc & (FF . cc) = ( QuotMSAlg (X(),R)) by A13, A45;

        hence thesis by A46;

      end;

      then P[XX] by A2, A3;

      hence P[A] by A1, A44, MSUALG_3: 17;

      thus F is_epimorphism (X(),A) by MSUALG_4: 3;

      then

       A47: F is "onto" by MSUALG_3:def 8;

      let B be non-empty MSAlgebra over S(), G be ManySortedFunction of X(), B such that

       A48: G is_homomorphism (X(),B) and

       A49: P[B];

      reconsider C = ( Image ( MSHomQuot G)) as strict non-empty MSSubAlgebra of B;

      

       A50: (( QuotMSAlg (X(),( MSCng G))),C) are_isomorphic by A48, MSUALG_4: 4, MSUALG_9: 16;

      

       A51: ( MSCng G) is Element of ( CongrLatt X()) by MSUALG_5:def 6;

      P[C] by A2, A49;

      then P[( QuotMSAlg (X(),( MSCng G)))] by A1, A50, MSUALG_3: 17;

      then ( MSCng G) in CC by A51;

      then R0 c= ( MSCng G) by CLOSURE2: 21, MSSUBFAM: 43;

      then

      consider H be ManySortedFunction of A, B such that

       A52: H is_homomorphism (A,B) and

       A53: G = (H ** F) by A48, MSUALG_9: 36;

      take H;

      thus H is_homomorphism (A,B) by A52;

      thus G = (H ** F) by A53;

      let K be ManySortedFunction of A, B;

      assume (K ** F) = G;

      hence thesis by A53, A47, EXTENS_1: 12;

    end;

    scheme :: BIRKHOFF:sch2

    ExFreeAlg2 { S() -> non empty non void ManySortedSign , X() -> non-empty ManySortedSet of the carrier of S() , P[ set] } :

ex A be strict non-empty MSAlgebra over S(), F be ManySortedFunction of X(), the Sorts of A st P[A] & for B be non-empty MSAlgebra over S() holds for G be ManySortedFunction of X(), the Sorts of B st P[B] holds ex H be ManySortedFunction of A, B st H is_homomorphism (A,B) & (H ** F) = G & for K be ManySortedFunction of A, B st K is_homomorphism (A,B) & (K ** F) = G holds H = K

      provided

       A1: for A,B be non-empty MSAlgebra over S() st (A,B) are_isomorphic & P[A] holds P[B]

       and

       A2: for A be non-empty MSAlgebra over S() holds for B be strict non-empty MSSubAlgebra of A st P[A] holds P[B]

       and

       A3: for I be set, 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) & P[A]) holds P[( product F)];

      

       A4: for A be non-empty MSAlgebra over S() holds for B be strict non-empty MSSubAlgebra of A st P[A] holds P[B] by A2;

      

       A5: for I be set, 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) & P[A]) holds P[( product F)] by A3;

      set FM = ( FreeMSA X());

      

       A6: ( Reverse X()) is "1-1" by MSUALG_9: 11;

      

       A7: for A,B be non-empty MSAlgebra over S() st (A,B) are_isomorphic & P[A] holds P[B] by A1;

      consider A be strict non-empty MSAlgebra over S(), F be ManySortedFunction of FM, A such that

       A8: P[A] and

       A9: F is_epimorphism (FM,A) and

       A10: for B be non-empty MSAlgebra over S() holds for G be ManySortedFunction of FM, B st G is_homomorphism (FM,B) & P[B] holds ex H be ManySortedFunction of A, B st H is_homomorphism (A,B) & (H ** F) = G & for K be ManySortedFunction of A, B st (K ** F) = G holds H = K from ExFreeAlg1( A7, A4, A5);

      reconsider R = ((F || ( FreeGen X())) ** (( Reverse X()) "" )) as ManySortedFunction of X(), the Sorts of A;

      take A;

      take R;

      thus P[A] by A8;

      let B be non-empty MSAlgebra over S(), G be ManySortedFunction of X(), the Sorts of B such that

       A11: P[B];

      consider GG be ManySortedFunction of FM, B such that

       A12: GG is_homomorphism (FM,B) and

       A13: (GG || ( FreeGen X())) = (G ** ( Reverse X())) by MSAFREE:def 5;

      consider H be ManySortedFunction of A, B such that

       A14: H is_homomorphism (A,B) and

       A15: (H ** F) = GG and for K be ManySortedFunction of A, B st (K ** F) = GG holds H = K by A10, A11, A12;

      take H;

      thus H is_homomorphism (A,B) by A14;

      

       A16: (H ** (F || ( FreeGen X()))) = (GG || ( FreeGen X())) by A15, EXTENS_1: 4;

      

       A17: F is "onto" by A9, MSUALG_3:def 8;

      ( rngs ( Reverse X())) = X() by EXTENS_1: 10;

      then

       A18: ( Reverse X()) is "onto" by EXTENS_1: 9;

      (R ** ( Reverse X())) = ((F || ( FreeGen X())) ** ((( Reverse X()) "" ) ** ( Reverse X()))) by PBOOLE: 140

      .= ((F || ( FreeGen X())) ** ( id ( FreeGen X()))) by A18, A6, MSUALG_3: 5

      .= (F || ( FreeGen X())) by MSUALG_3: 3;

      then

       A19: ((H ** R) ** ( Reverse X())) = (G ** ( Reverse X())) by A13, A16, PBOOLE: 140;

      hence (H ** R) = G by A18, EXTENS_1: 12;

      let K be ManySortedFunction of A, B;

      assume

       A20: K is_homomorphism (A,B);

      assume (K ** R) = G;

      then (K ** (((F || ( FreeGen X())) ** (( Reverse X()) "" )) ** ( Reverse X()))) = ((H ** ((F || ( FreeGen X())) ** (( Reverse X()) "" ))) ** ( Reverse X())) by A19, PBOOLE: 140;

      then (K ** (((F || ( FreeGen X())) ** (( Reverse X()) "" )) ** ( Reverse X()))) = (H ** (((F || ( FreeGen X())) ** (( Reverse X()) "" )) ** ( Reverse X()))) by PBOOLE: 140;

      then (K ** ((F || ( FreeGen X())) ** ((( Reverse X()) "" ) ** ( Reverse X())))) = (H ** (((F || ( FreeGen X())) ** (( Reverse X()) "" )) ** ( Reverse X()))) by PBOOLE: 140;

      then (K ** ((F || ( FreeGen X())) ** ((( Reverse X()) "" ) ** ( Reverse X())))) = (H ** ((F || ( FreeGen X())) ** ((( Reverse X()) "" ) ** ( Reverse X())))) by PBOOLE: 140;

      then (K ** ((F || ( FreeGen X())) ** ( id ( FreeGen X())))) = (H ** ((F || ( FreeGen X())) ** ((( Reverse X()) "" ) ** ( Reverse X())))) by A18, A6, MSUALG_3: 5;

      then (K ** ((F || ( FreeGen X())) ** ( id ( FreeGen X())))) = (H ** ((F || ( FreeGen X())) ** ( id ( FreeGen X())))) by A18, A6, MSUALG_3: 5;

      then (K ** (F || ( FreeGen X()))) = (H ** ((F || ( FreeGen X())) ** ( id ( FreeGen X())))) by MSUALG_3: 3;

      then (K ** (F || ( FreeGen X()))) = (H ** (F || ( FreeGen X()))) by MSUALG_3: 3;

      then ((K ** F) || ( FreeGen X())) = (H ** (F || ( FreeGen X()))) by EXTENS_1: 4;

      then

       A21: ((K ** F) || ( FreeGen X())) = ((H ** F) || ( FreeGen X())) by EXTENS_1: 4;

      F is_homomorphism (FM,A) by A9, MSUALG_3:def 8;

      then (K ** F) is_homomorphism (FM,B) by A20, MSUALG_3: 10;

      then (K ** F) = (H ** F) by A12, A15, A21, EXTENS_1: 14;

      hence thesis by A17, EXTENS_1: 12;

    end;

    scheme :: BIRKHOFF:sch3

    Exhash { S() -> non empty non void ManySortedSign , F,A() -> non-empty MSAlgebra over S() , fi() -> ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of F() , a() -> ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of A() , P[ set] } :

ex H be ManySortedFunction of F(), A() st H is_homomorphism (F(),A()) & (a() -hash ) = (H ** (fi() -hash ))

      provided

       A1: P[A()]

       and

       A2: for C be non-empty MSAlgebra over S() holds for G be ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of C st P[C] holds ex h be ManySortedFunction of F(), C st h is_homomorphism (F(),C) & G = (h ** fi());

      consider H be ManySortedFunction of F(), A() such that

       A3: H is_homomorphism (F(),A()) and

       A4: a() = (H ** fi()) by A1, A2;

      take H;

      thus H is_homomorphism (F(),A()) by A3;

      (fi() -hash ) is_homomorphism (( FreeMSA (the carrier of S() --> NAT )),F()) by Def1;

      then

       A5: (H ** (fi() -hash )) is_homomorphism (( FreeMSA (the carrier of S() --> NAT )),A()) by A3, MSUALG_3: 10;

      reconsider SN = (the carrier of S() --> NAT ) as non-empty ManySortedSet of the carrier of S();

      reconsider h1 = a() as ManySortedFunction of SN, the Sorts of A();

      

       A6: (h1 -hash ) is_homomorphism (( FreeMSA SN),A()) by Def1;

      ((h1 -hash ) || ( FreeGen SN)) = (a() ** ( Reverse SN)) by Def1

      .= (H ** (fi() ** ( Reverse SN))) by A4, PBOOLE: 140

      .= (H ** ((fi() -hash ) || ( FreeGen (the carrier of S() --> NAT )))) by Def1

      .= ((H ** (fi() -hash )) || ( FreeGen (the carrier of S() --> NAT ))) by EXTENS_1: 4;

      hence thesis by A6, A5, EXTENS_1: 14;

    end;

    scheme :: BIRKHOFF:sch4

    EqTerms { S() -> non empty non void ManySortedSign , F() -> non-empty MSAlgebra over S() , fi() -> ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of F() , s() -> SortSymbol of S() , t1,t2() -> Element of (the Sorts of ( TermAlg S()) . s()) , P[ set] } :

for B be non-empty MSAlgebra over S() st P[B] holds B |= (t1() '=' t2())

      provided

       A1: (((fi() -hash ) . s()) . t1()) = (((fi() -hash ) . s()) . t2())

       and

       A2: for C be non-empty MSAlgebra over S() holds for G be ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of C st P[C] holds ex h be ManySortedFunction of F(), C st h is_homomorphism (F(),C) & G = (h ** fi());

      reconsider fi1 = fi() as ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of F();

      reconsider SN = (the carrier of S() --> NAT ) as non-empty ManySortedSet of the carrier of S();

      let B be non-empty MSAlgebra over S();

      assume P[B];

      then

       A3: P[B];

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

       A4: h is_homomorphism (( TermAlg S()),B);

      reconsider h1 = h as ManySortedFunction of ( FreeMSA SN), B;

      set alfa = ((h1 || ( FreeGen SN)) ** (( Reverse SN) "" ));

      

       A5: (alfa -hash ) is_homomorphism (( FreeMSA SN),B) by Def1;

      reconsider alfa1 = alfa as ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of B;

      

       A6: for C be non-empty MSAlgebra over S() holds for G be ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of C st P[C] holds ex h be ManySortedFunction of F(), C st h is_homomorphism (F(),C) & G = (h ** fi1) by A2;

      consider H be ManySortedFunction of F(), B such that H is_homomorphism (F(),B) and

       A7: (alfa1 -hash ) = (H ** (fi1 -hash )) from Exhash( A3, A6);

      

       A8: (((alfa -hash ) . s()) . t1()) = (((H . s()) * ((fi() -hash ) . s())) . t1()) by A7, MSUALG_3: 2

      .= ((H . s()) . (((fi() -hash ) . s()) . t2())) by A1, FUNCT_2: 15

      .= (((H . s()) * ((fi() -hash ) . s())) . t2()) by FUNCT_2: 15

      .= (((alfa -hash ) . s()) . t2()) by A7, MSUALG_3: 2;

      ( rngs ( Reverse SN)) = SN by EXTENS_1: 10;

      then

       A9: ( Reverse SN) is "1-1" "onto" by EXTENS_1: 9, MSUALG_9: 11;

      ((alfa -hash ) || ( FreeGen SN)) = (alfa ** ( Reverse SN)) by Def1

      .= ((h1 || ( FreeGen SN)) ** ((( Reverse SN) "" ) ** ( Reverse SN))) by PBOOLE: 140

      .= ((h1 || ( FreeGen SN)) ** ( id ( FreeGen SN))) by A9, MSUALG_3: 5

      .= (h1 || ( FreeGen SN)) by MSUALG_3: 3;

      then

       A10: (alfa -hash ) = h1 by A4, A5, EXTENS_1: 14;

      

      thus ((h . s()) . ( [t1(), t2()] `1 )) = ((h . s()) . t1())

      .= ((h . s()) . ( [t1(), t2()] `2 )) by A10, A8;

    end;

    scheme :: BIRKHOFF:sch5

    FreeIsGen { S() -> non empty non void ManySortedSign , X() -> non-empty ManySortedSet of the carrier of S() , A() -> strict non-empty MSAlgebra over S() , f() -> ManySortedFunction of X(), the Sorts of A() , P[ set] } :

(f() .:.: X()) is non-empty GeneratorSet of A()

      provided

       A1: for C be non-empty MSAlgebra over S() holds for G be ManySortedFunction of X(), the Sorts of C st P[C] holds ex H be ManySortedFunction of A(), C st H is_homomorphism (A(),C) & (H ** f()) = G & for K be ManySortedFunction of A(), C st K is_homomorphism (A(),C) & (K ** f()) = G holds H = K

       and

       A2: P[A()]

       and

       A3: for A be non-empty MSAlgebra over S() holds for B be strict non-empty MSSubAlgebra of A st P[A] holds P[B];

      set I = the carrier of S();

      

       A4: (f() .:.: X()) is non-empty

      proof

        let i be object;

        assume

         A5: i in I;

        then

        reconsider fi = (f() . i) as Function of (X() . i), (the Sorts of A() . i) by PBOOLE:def 15;

        

         A6: ((f() .:.: X()) . i) = (fi .: (X() . i)) by A5, PBOOLE:def 20;

        reconsider Xi = (X() . i) as non empty set by A5;

        

         A7: Xi meets Xi;

        ( dom fi) = Xi by A5, FUNCT_2:def 1;

        hence thesis by A7, A6, RELAT_1: 118;

      end;

      (f() .:.: X()) is ManySortedSubset of the Sorts of A()

      proof

        let i be object;

        assume

         A8: i in I;

        then

        reconsider fi = (f() . i) as Function of (X() . i), (the Sorts of A() . i) by PBOOLE:def 15;

        ((f() .:.: X()) . i) = (fi .: (X() . i)) by A8, PBOOLE:def 20;

        hence thesis;

      end;

      then

      reconsider Gen = (f() .:.: X()) as non-empty MSSubset of A() by A4;

      set AA = ( GenMSAlg Gen);

      

       A9: X() is_transformable_to the Sorts of AA;

      X() is_transformable_to the Sorts of A();

      then

       A10: ( doms f()) = X() by MSSUBFAM: 17;

      then ( rngs f()) = (f() .:.: X()) by EQUATION: 13;

      then ( rngs f()) is ManySortedSubset of the Sorts of AA by MSUALG_2:def 17;

      then ( rngs f()) c= the Sorts of AA by PBOOLE:def 18;

      then

      reconsider iN = f() as ManySortedFunction of X(), the Sorts of AA by A9, A10, EQUATION: 4;

      consider IN be ManySortedFunction of A(), AA such that

       A11: IN is_homomorphism (A(),AA) and

       A12: (IN ** f()) = iN and for K be ManySortedFunction of A(), AA st K is_homomorphism (A(),AA) & (K ** f()) = iN holds IN = K by A1, A2, A3;

      the Sorts of AA is ManySortedSubset of the Sorts of A() by MSUALG_2:def 9;

      then

      reconsider h = ( id the Sorts of AA) as ManySortedFunction of AA, A() by EXTENS_1: 5;

      consider HIN be ManySortedFunction of A(), A() such that HIN is_homomorphism (A(),A()) and (HIN ** f()) = (h ** iN) and

       A13: for K be ManySortedFunction of A(), A() st K is_homomorphism (A(),A()) & (K ** f()) = (h ** iN) holds HIN = K by A1, A2;

      h is_monomorphism (AA,A()) by MSUALG_3: 22;

      then

       A14: h is_homomorphism (AA,A()) by MSUALG_3:def 9;

      reconsider hIN = (h ** IN) as ManySortedFunction of A(), A();

      (h ** iN) = ((h ** IN) ** f()) by A12, PBOOLE: 140;

      then

       A15: HIN = hIN by A11, A13, A14, MSUALG_3: 10;

      

       A16: A() is MSSubAlgebra of A() by MSUALG_2: 5;

      f() = (h ** iN) by MSUALG_3: 4;

      then (( id the Sorts of A()) ** f()) = (h ** iN) by MSUALG_3: 4;

      then HIN = ( id the Sorts of A()) by A13, MSUALG_3: 9;

      then

       A17: HIN is "onto";

      the Sorts of AA = (h .:.: the Sorts of AA) by EQUATION: 15

      .= the Sorts of A() by A15, A17, EQUATION: 2, EQUATION: 9;

      then AA = A() by A16, MSUALG_2: 9;

      hence thesis by MSAFREE: 3;

    end;

    scheme :: BIRKHOFF:sch6

    Hashisonto { S() -> non empty non void ManySortedSign , A() -> strict non-empty MSAlgebra over S() , F() -> ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of A() , P[ set] } :

(F() -hash ) is_epimorphism (( FreeMSA (the carrier of S() --> NAT )),A())

      provided

       A1: for C be non-empty MSAlgebra over S() holds for G be ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of C st P[C] holds ex H be ManySortedFunction of A(), C st H is_homomorphism (A(),C) & (H ** F()) = G & for K be ManySortedFunction of A(), C st K is_homomorphism (A(),C) & (K ** F()) = G holds H = K

       and

       A2: P[A()]

       and

       A3: for A be non-empty MSAlgebra over S() holds for B be strict non-empty MSSubAlgebra of A st P[A] holds P[B];

      

       A4: P[A()] by A2;

      set V = (the carrier of S() --> NAT );

      reconsider Gen = the Sorts of ( FreeMSA V) as GeneratorSet of ( FreeMSA V) by MSAFREE2: 6;

      

       A5: (F() .:.: V) c= ( rngs F()) by EQUATION: 12;

      the Sorts of ( FreeMSA V) is_transformable_to the Sorts of A();

      then ( doms (F() -hash )) = the Sorts of ( FreeMSA V) by MSSUBFAM: 17;

      then

       A6: ((F() -hash ) .:.: the Sorts of ( FreeMSA V)) = ( rngs (F() -hash )) by EQUATION: 13;

      ( rngs F()) c= ( rngs (F() -hash )) by Th1;

      then

       A7: (F() .:.: V) c= ((F() -hash ) .:.: Gen) by A6, A5, PBOOLE: 13;

      

       A8: (F() -hash ) is_homomorphism (( FreeMSA V),A()) by Def1;

      

       A9: for A be non-empty MSAlgebra over S() holds for B be strict non-empty MSSubAlgebra of A st P[A] holds P[B] by A3;

      

       A10: for C be non-empty MSAlgebra over S() holds for G be ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of C st P[C] holds ex H be ManySortedFunction of A(), C st H is_homomorphism (A(),C) & (H ** F()) = G & for K be ManySortedFunction of A(), C st K is_homomorphism (A(),C) & (K ** F()) = G holds H = K by A1;

      (F() .:.: V) is non-empty GeneratorSet of A() from FreeIsGen( A10, A4, A9);

      hence thesis by A7, A8, EQUATION: 23;

    end;

    scheme :: BIRKHOFF:sch7

    FinGenAlgInVar { S() -> non empty non void ManySortedSign , A() -> strict finitely-generated non-empty MSAlgebra over S() , F() -> non-empty MSAlgebra over S() , fi() -> ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of F() , P,Q[ set] } :

P[A()]

      provided

       A1: Q[A()]

       and

       A2: P[F()]

       and

       A3: for C be non-empty MSAlgebra over S() holds for G be ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of C st Q[C] holds ex h be ManySortedFunction of F(), C st h is_homomorphism (F(),C) & G = (h ** fi())

       and

       A4: for A,B be non-empty MSAlgebra over S() st (A,B) are_isomorphic & P[A] holds P[B]

       and

       A5: for A be non-empty MSAlgebra over S(), R be MSCongruence of A st P[A] holds P[( QuotMSAlg (A,R))];

      set I = the carrier of S(), sA = the Sorts of A();

      consider Gen be GeneratorSet of A() such that

       A6: Gen is finite-yielding by MSAFREE2:def 10;

      reconsider Gen as finite-yielding ManySortedSubset of sA by A6;

      consider GEN be non-empty finite-yielding ManySortedSubset of sA such that

       A7: Gen c= GEN by MSUALG_9: 7;

      consider F be ManySortedFunction of (I --> NAT ), GEN such that

       A8: F is "onto" by MSUALG_9: 12;

      (I --> NAT ) is_transformable_to GEN;

      then

      reconsider G = F as ManySortedFunction of (I --> NAT ), sA by EXTENS_1: 5;

      consider h be ManySortedFunction of F(), A() such that

       A9: h is_homomorphism (F(),A()) and

       A10: G = (h ** fi()) by A1, A3;

      reconsider sI1 = the Sorts of ( Image h) as MSSubset of ( Image h) by PBOOLE:def 18;

      

       A11: GEN is GeneratorSet of A() by A7, MSSCYC_1: 21;

      reconsider sI = the Sorts of ( Image h) as MSSubset of A() by MSUALG_2:def 9;

      GEN is ManySortedSubset of sI

      proof

        let i be object;

        assume i in I;

        then

        reconsider s = i as SortSymbol of S();

        let g be object;

        assume

         A12: g in (GEN . i);

        reconsider fi = (fi() . s) as sequence of (the Sorts of F() . s);

        ( dom ((h . s) * fi)) = NAT by FUNCT_2:def 1

        .= ( dom fi) by FUNCT_2:def 1;

        then

         A14: ( rng fi) c= ( dom (h . s)) by FUNCT_1: 15;

        ( rng (F . s)) = (GEN . s) by A8, MSUALG_3:def 3;

        then

        consider x be object such that

         A15: x in ( dom (F . s)) and

         A16: g = ((F . s) . x) by A12, FUNCT_1:def 3;

        ( dom (F . s)) = NAT by FUNCT_2:def 1

        .= ( dom fi) by FUNCT_2:def 1;

        then

         A17: (fi . x) in ( rng fi) by A15, FUNCT_1:def 3;

        g = (((h . s) * fi) . x) by A10, A16, MSUALG_3: 2

        .= ((h . s) . (fi . x)) by A15, FUNCT_2: 15;

        then g in ((h . s) .: (the Sorts of F() . s)) by A17, A14, FUNCT_1:def 6;

        then g in ((h .:.: the Sorts of F()) . s) by PBOOLE:def 20;

        hence thesis by A9, MSUALG_3:def 12;

      end;

      then

       A18: ( GenMSAlg GEN) is MSSubAlgebra of ( GenMSAlg sI) by EXTENS_1: 17;

      ( GenMSAlg sI) = ( GenMSAlg sI1) by EXTENS_1: 18;

      then ( GenMSAlg GEN) is MSSubAlgebra of ( Image h) by A18, MSUALG_2: 21;

      then A() is MSSubAlgebra of ( Image h) by A11, MSAFREE: 3;

      then A() = ( Image h) by MSUALG_2: 7;

      then

       A19: h is_epimorphism (F(),A()) by A9, MSUALG_3: 19;

      P[( QuotMSAlg (F(),( MSCng h)))] by A2, A5;

      hence thesis by A4, A19, MSUALG_4: 6;

    end;

    scheme :: BIRKHOFF:sch8

    QuotEpi { S() -> non empty non void ManySortedSign , X,Y() -> non-empty MSAlgebra over S() , P[ set] } :

P[Y()]

      provided

       A1: ex H be ManySortedFunction of X(), Y() st H is_epimorphism (X(),Y())

       and

       A2: P[X()]

       and

       A3: for A,B be non-empty MSAlgebra over S() st (A,B) are_isomorphic & P[A] holds P[B]

       and

       A4: for A be non-empty MSAlgebra over S(), R be MSCongruence of A st P[A] holds P[( QuotMSAlg (A,R))];

      consider H be ManySortedFunction of X(), Y() such that

       A5: H is_epimorphism (X(),Y()) by A1;

      P[( QuotMSAlg (X(),( MSCng H)))] by A2, A4;

      hence thesis by A3, A5, MSUALG_4: 6;

    end;

    scheme :: BIRKHOFF:sch9

    AllFinGen { S() -> non empty non void ManySortedSign , X() -> non-empty MSAlgebra over S() , P[ set] } :

P[X()]

      provided

       A1: for B be strict non-empty finitely-generated MSSubAlgebra of X() holds P[B]

       and

       A2: for A,B be non-empty MSAlgebra over S() st (A,B) are_isomorphic & P[A] holds P[B]

       and

       A3: for A be non-empty MSAlgebra over S() holds for B be strict non-empty MSSubAlgebra of A st P[A] holds P[B]

       and

       A4: for A be non-empty MSAlgebra over S(), R be MSCongruence of A st P[A] holds P[( QuotMSAlg (A,R))]

       and

       A5: for I be set, 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) & P[A]) holds P[( product F)];

      

       A6: for A,B be non-empty MSAlgebra over S() st (A,B) are_isomorphic & P[A] holds P[B] by A2;

      set T = the strict non-empty finitely-generated MSSubAlgebra of X();

      set CC = { C where C be Element of ( MSSub X()) : ex R be strict non-empty finitely-generated MSSubAlgebra of X() st R = C };

      T in ( MSSub X()) by MSUALG_2:def 19;

      then T in CC;

      then

      reconsider CC as non empty set;

      defpred P[ object, object] means $1 = $2;

      

       A7: for c be object st c in CC holds ex j be object st P[c, j];

      consider FF be ManySortedSet of CC such that

       A8: for c be object st c in CC holds P[c, (FF . c)] from PBOOLE:sch 3( A7);

      FF is MSAlgebra-Family of CC, S()

      proof

        let c be object;

        assume

         A9: c in CC;

        then ex Q be Element of ( MSSub X()) st c = Q & ex R be strict non-empty finitely-generated MSSubAlgebra of X() st R = Q;

        hence thesis by A8, A9;

      end;

      then

      reconsider FF as MSAlgebra-Family of CC, S();

      consider prSOR be strict non-empty MSSubAlgebra of ( product FF) such that

       A10: ex BA be ManySortedFunction of prSOR, X() st BA is_epimorphism (prSOR,X()) by A8, EQUATION: 27;

      

       A11: for A be non-empty MSAlgebra over S(), R be MSCongruence of A st P[A] holds P[( QuotMSAlg (A,R))] by A4;

      for i be set st i in CC holds ex A be MSAlgebra over S() st A = (FF . i) & P[A]

      proof

        let i be set;

        assume

         A12: i in CC;

        then

        consider Q be Element of ( MSSub X()) such that

         A13: i = Q and

         A14: ex R be strict non-empty finitely-generated MSSubAlgebra of X() st R = Q;

        consider R be strict non-empty finitely-generated MSSubAlgebra of X() such that

         A15: R = Q by A14;

        take R;

        thus thesis by A1, A8, A12, A13, A15;

      end;

      then

       A16: P[prSOR] by A3, A5;

      thus P[X()] from QuotEpi( A10, A16, A6, A11);

    end;

    scheme :: BIRKHOFF:sch10

    FreeInModIsInVar1 { S() -> non empty non void ManySortedSign , X() -> non-empty MSAlgebra over S() , P,Q[ set] } :

Q[X()]

      provided

       A1: for A be non-empty MSAlgebra over S() holds Q[A] iff for s be SortSymbol of S(), e be Element of (( Equations S()) . s) st (for B be non-empty MSAlgebra over S() st P[B] holds B |= e) holds A |= e

       and

       A2: P[X()];

      for s be SortSymbol of S(), e be Element of (( Equations S()) . s) st (for B be non-empty MSAlgebra over S() st P[B] holds B |= e) holds X() |= e by A2;

      hence thesis by A1;

    end;

    scheme :: BIRKHOFF:sch11

    FreeInModIsInVar { S() -> non empty non void ManySortedSign , X() -> strict non-empty MSAlgebra over S() , psi() -> ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of X() , P,Q[ set] } :

P[X()]

      provided

       A1: for A be non-empty MSAlgebra over S() holds Q[A] iff for s be SortSymbol of S(), e be Element of (( Equations S()) . s) st (for B be non-empty MSAlgebra over S() st P[B] holds B |= e) holds A |= e

       and

       A2: for C be non-empty MSAlgebra over S() holds for G be ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of C st Q[C] holds ex H be ManySortedFunction of X(), C st H is_homomorphism (X(),C) & (H ** psi()) = G & for K be ManySortedFunction of X(), C st K is_homomorphism (X(),C) & (K ** psi()) = G holds H = K

       and

       A3: Q[X()]

       and

       A4: for A,B be non-empty MSAlgebra over S() st (A,B) are_isomorphic & P[A] holds P[B]

       and

       A5: for A be non-empty MSAlgebra over S() holds for B be strict non-empty MSSubAlgebra of A st P[A] holds P[B]

       and

       A6: for I be set, 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) & P[A]) holds P[( product F)];

      

       A7: for I be set, 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) & P[A]) holds P[( product F)] by A6;

      set V = (the carrier of S() --> NAT );

      

       A8: for A be non-empty MSAlgebra over S() holds for B be strict non-empty MSSubAlgebra of A st P[A] holds P[B] by A5;

      

       A9: for A,B be non-empty MSAlgebra over S() st (A,B) are_isomorphic & P[A] holds P[B] by A4;

      consider A be strict non-empty MSAlgebra over S(), fi be ManySortedFunction of V, the Sorts of A such that

       A10: P[A] and

       A11: for B be non-empty MSAlgebra over S() holds for G be ManySortedFunction of V, the Sorts of B st P[B] holds ex H be ManySortedFunction of A, B st H is_homomorphism (A,B) & (H ** fi) = G & for K be ManySortedFunction of A, B st K is_homomorphism (A,B) & (K ** fi) = G holds H = K from ExFreeAlg2( A9, A8, A7);

      

       A12: for C be non-empty MSAlgebra over S() holds for G be ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of C st Q[C] holds ex H be ManySortedFunction of X(), C st H is_homomorphism (X(),C) & (H ** psi()) = G & for K be ManySortedFunction of X(), C st K is_homomorphism (X(),C) & (K ** psi()) = G holds H = K by A2;

      

       A13: for C be non-empty MSAlgebra over S() holds for G be ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of C st Q[C] holds ex h be ManySortedFunction of X(), C st h is_homomorphism (X(),C) & G = (h ** psi())

      proof

        let C be non-empty MSAlgebra over S(), G be ManySortedFunction of V, the Sorts of C;

        assume Q[C];

        then

        consider h be ManySortedFunction of X(), C such that

         A14: h is_homomorphism (X(),C) and

         A15: G = (h ** psi()) and for K be ManySortedFunction of X(), C st K is_homomorphism (X(),C) & (K ** psi()) = G holds h = K by A2;

        take h;

        thus thesis by A14, A15;

      end;

      

       A16: Q[X()] by A3;

      

       A17: for A be non-empty MSAlgebra over S() holds Q[A] iff for s be SortSymbol of S(), e be Element of (( Equations S()) . s) st (for B be non-empty MSAlgebra over S() st P[B] holds B |= e) holds A |= e by A1;

      

       A18: Q[A] from FreeInModIsInVar1( A17, A10);

      consider H be ManySortedFunction of X(), A such that

       A19: H is_homomorphism (X(),A) and

       A20: (fi -hash ) = (H ** (psi() -hash )) from Exhash( A18, A13);

      

       A21: (psi() -hash ) is_homomorphism (( FreeMSA V),X()) by Def1;

      now

        let i be set;

        assume i in the carrier of S();

        then

        reconsider s = i as SortSymbol of S();

        thus (H . i) is one-to-one

        proof

          

           A22: for D be non-empty MSAlgebra over S() holds for E be strict non-empty MSSubAlgebra of D holds Q[D] implies Q[E]

          proof

            let D be non-empty MSAlgebra over S(), E be strict non-empty MSSubAlgebra of D such that

             A23: Q[D];

            for s be SortSymbol of S(), e be Element of (( Equations S()) . s) st for B be non-empty MSAlgebra over S() st P[B] holds B |= e holds E |= e by A1, A23, EQUATION: 31;

            hence thesis by A1;

          end;

          (psi() -hash ) is_epimorphism (( FreeMSA V),X()) from Hashisonto( A12, A16, A22);

          then

           A24: (psi() -hash ) is "onto" by MSUALG_3:def 8;

          

           A25: for C be non-empty MSAlgebra over S() holds for G be ManySortedFunction of V, the Sorts of C st P[C] holds ex H be ManySortedFunction of A, C st H is_homomorphism (A,C) & G = (H ** fi)

          proof

            let C be non-empty MSAlgebra over S(), G be ManySortedFunction of V, the Sorts of C;

            assume P[C];

            then

            consider H be ManySortedFunction of A, C such that

             A26: H is_homomorphism (A,C) and

             A27: (H ** fi) = G and for K be ManySortedFunction of A, C st K is_homomorphism (A,C) & (K ** fi) = G holds H = K by A11;

            take H;

            thus thesis by A26, A27;

          end;

          let a,b be object such that

           A28: a in ( dom (H . i)) and

           A29: b in ( dom (H . i)) and

           A30: ((H . i) . a) = ((H . i) . b);

          

           A31: ( dom (H . s)) = (the Sorts of X() . s) by FUNCT_2:def 1

          .= ( rng ((psi() -hash ) . s)) by A24, MSUALG_3:def 3;

          then

          consider t1 be object such that

           A32: t1 in ( dom ((psi() -hash ) . s)) and

           A33: (((psi() -hash ) . s) . t1) = a by A28, FUNCT_1:def 3;

          consider t2 be object such that

           A34: t2 in ( dom ((psi() -hash ) . s)) and

           A35: (((psi() -hash ) . s) . t2) = b by A29, A31, FUNCT_1:def 3;

          reconsider t1, t2 as Element of (the Sorts of ( TermAlg S()) . s) by A32, A34;

          set e = (t1 '=' t2);

          

           A36: (((fi -hash ) . s) . t1) = (((H . s) * ((psi() -hash ) . s)) . t1) by A20, MSUALG_3: 2

          .= ((H . s) . a) by A33, FUNCT_2: 15

          .= (((H . s) * ((psi() -hash ) . s)) . t2) by A30, A35, FUNCT_2: 15

          .= (((fi -hash ) . s) . t2) by A20, MSUALG_3: 2;

          for B be non-empty MSAlgebra over S() st P[B] holds B |= (t1 '=' t2) from EqTerms( A36, A25);

          then

           A37: X() |= e by A1, A3;

          

          thus a = (((psi() -hash ) . s) . (e `1 )) by A33

          .= (((psi() -hash ) . s) . (e `2 )) by A21, A37

          .= b by A35;

        end;

      end;

      then H is "1-1" by MSUALG_3: 1;

      then H is_monomorphism (X(),A) by A19, MSUALG_3:def 9;

      then

       A38: (X(),( Image H)) are_isomorphic by MSUALG_9: 16;

      P[( Image H)] by A5, A10;

      hence thesis by A4, A38, MSUALG_3: 17;

    end;

    ::$Notion-Name

    scheme :: BIRKHOFF:sch12

    Birkhoff { S() -> non empty non void ManySortedSign , P[ set] } :

ex E be EqualSet of S() st for A be non-empty MSAlgebra over S() holds P[A] iff A |= E

      provided

       A1: for A,B be non-empty MSAlgebra over S() st (A,B) are_isomorphic & P[A] holds P[B]

       and

       A2: for A be non-empty MSAlgebra over S() holds for B be strict non-empty MSSubAlgebra of A st P[A] holds P[B]

       and

       A3: for A be non-empty MSAlgebra over S(), R be MSCongruence of A st P[A] holds P[( QuotMSAlg (A,R))]

       and

       A4: for I be set, 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) & P[A]) holds P[( product F)];

      

       A5: for A be non-empty MSAlgebra over S() holds for B be strict non-empty MSSubAlgebra of A st P[A] holds P[B] by A2;

      set XX = (the carrier of S() --> NAT );

      set I = the carrier of S();

      defpred R[ object, object] means ex s be SortSymbol of S() st $1 = s & $2 = { e where e be Element of (( Equations S()) . s) : for A be non-empty MSAlgebra over S() holds P[A] implies A |= e };

       A6:

      now

        let w be object;

        assume w in I;

        then

        consider s be SortSymbol of S() such that

         A7: s = w;

        reconsider d = { e where e be Element of (( Equations S()) . s) : for A be non-empty MSAlgebra over S() holds P[A] implies A |= e } as object;

        take d;

        thus R[w, d] by A7;

      end;

      consider E be ManySortedSet of I such that

       A8: for i be object st i in I holds R[i, (E . i)] from PBOOLE:sch 3( A6);

      E is ManySortedSubset of ( Equations S())

      proof

        let j be object;

        assume j in I;

        then

        consider s be SortSymbol of S() such that

         A9: j = s and

         A10: (E . j) = { e where e be Element of (( Equations S()) . s) : for A be non-empty MSAlgebra over S() holds P[A] implies A |= e } by A8;

        let q be object;

        assume q in (E . j);

        then ex z be Element of (( Equations S()) . s) st q = z & for A be non-empty MSAlgebra over S() holds P[A] implies A |= z by A10;

        hence thesis by A9;

      end;

      then

      reconsider E as EqualSet of S();

      

       A11: for A,B be non-empty MSAlgebra over S() st (A,B) are_isomorphic & P[A] holds P[B] by A1;

      defpred Q[ MSAlgebra over S()] means $1 |= E;

      

       A12: for D be non-empty MSAlgebra over S() holds Q[D] iff for s be SortSymbol of S(), e be Element of (( Equations S()) . s) st (for M be non-empty MSAlgebra over S() st P[M] holds M |= e) holds D |= e

      proof

        let D be non-empty MSAlgebra over S();

        thus Q[D] implies for s be SortSymbol of S(), e be Element of (( Equations S()) . s) st (for B be non-empty MSAlgebra over S() st P[B] holds B |= e) holds D |= e

        proof

          assume

           A13: Q[D];

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

           A14: for B be non-empty MSAlgebra over S() st P[B] holds B |= e;

           R[s, (E . s)] by A8;

          then e in (E . s) by A14;

          hence thesis by A13, EQUATION:def 6;

        end;

        assume

         A15: for s be SortSymbol of S(), e be Element of (( Equations S()) . s) st (for B be non-empty MSAlgebra over S() st P[B] holds B |= e) holds D |= e;

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

         A16: e in (E . s);

         R[s, (E . s)] by A8;

        then ex f be Element of (( Equations S()) . s) st e = f & for A be non-empty MSAlgebra over S() holds P[A] implies A |= f by A16;

        hence thesis by A15;

      end;

      

       A17: for A be non-empty MSAlgebra over S() holds for B be strict non-empty MSSubAlgebra of A holds Q[A] implies Q[B] by EQUATION: 32;

      

       A18: for I be set, F be MSAlgebra-Family of I, S() holds (for i be set st i in I holds ex A be MSAlgebra over S() st A = (F . i) & Q[A]) implies Q[( product F)] by EQUATION: 38;

      

       A19: for A,B be non-empty MSAlgebra over S() st (A,B) are_isomorphic holds Q[A] implies Q[B] by EQUATION: 34;

      consider K be strict non-empty MSAlgebra over S(), F be ManySortedFunction of XX, the Sorts of K such that

       A20: Q[K] and

       A21: for B be non-empty MSAlgebra over S() holds for G be ManySortedFunction of XX, the Sorts of B st Q[B] holds ex H be ManySortedFunction of K, B st H is_homomorphism (K,B) & (H ** F) = G & for W be ManySortedFunction of K, B st W is_homomorphism (K,B) & (W ** F) = G holds H = W from ExFreeAlg2( A19, A17, A18);

      

       A22: for M be non-empty MSAlgebra over S() holds for G be ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of M st Q[M] holds ex H be ManySortedFunction of K, M st H is_homomorphism (K,M) & G = (H ** F)

      proof

        let M be non-empty MSAlgebra over S(), G be ManySortedFunction of (the carrier of S() --> NAT ), the Sorts of M;

        assume Q[M];

        then ex H be ManySortedFunction of K, M st H is_homomorphism (K,M) & (H ** F) = G & for W be ManySortedFunction of K, M st W is_homomorphism (K,M) & (W ** F) = G holds H = W by A21;

        hence ex H be ManySortedFunction of K, M st H is_homomorphism (K,M) & (H ** F) = G;

      end;

      

       A23: for I be set, 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) & P[A]) holds P[( product F)] by A4;

      take E;

      let A be non-empty MSAlgebra over S();

      hereby

        assume

         A24: P[A];

        thus A |= E

        proof

          let s1 be SortSymbol of S();

          

           A25: R[s1, (E . s1)] by A8;

          let e be Element of (( Equations S()) . s1);

          assume e in (E . s1);

          then

          consider x be Element of (( Equations S()) . s1) such that

           A26: e = x and

           A27: for A be non-empty MSAlgebra over S() holds P[A] implies A |= x by A25;

          

           A28: A |= x by A24, A27;

          let h be ManySortedFunction of ( TermAlg S()), A;

          assume h is_homomorphism (( TermAlg S()),A);

          hence thesis by A26, A28;

        end;

      end;

      assume

       A29: A |= E;

      

       A30: for A be non-empty MSAlgebra over S(), R be MSCongruence of A st P[A] holds P[( QuotMSAlg (A,R))] by A3;

      

       A31: Q[K] by A20;

      

       A32: P[K] from FreeInModIsInVar( A12, A21, A31, A11, A5, A23);

      

       A33: for B be strict non-empty finitely-generated MSSubAlgebra of A holds P[B]

      proof

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

        

         A34: Q[B] by A29, EQUATION: 32;

        thus P[B] from FinGenAlgInVar( A34, A32, A22, A11, A30);

      end;

      thus P[A] from AllFinGen( A33, A11, A5, A30, A23);

    end;