:: BIRKHOFF semantic presentation begin definition let S be non empty non void ManySortedSign ; let X be V2() ManySortedSet of the carrier of S; let A be non-empty MSAlgebra over S; let F be ManySortedFunction of X, the Sorts of A; funcF -hash -> ManySortedFunction of (FreeMSA X),A means :Def1: :: BIRKHOFF:def 1 ( it is_homomorphism FreeMSA X,A & it || (FreeGen X) = F ** (Reverse X) ); existence ex b1 being ManySortedFunction of (FreeMSA X),A st ( b1 is_homomorphism FreeMSA X,A & b1 || (FreeGen X) = F ** (Reverse X) ) by MSAFREE:def_5; uniqueness for b1, b2 being ManySortedFunction of (FreeMSA X),A st b1 is_homomorphism FreeMSA X,A & b1 || (FreeGen X) = F ** (Reverse X) & b2 is_homomorphism FreeMSA X,A & b2 || (FreeGen X) = F ** (Reverse X) holds b1 = b2 by EXTENS_1:14; end; :: deftheorem Def1 defines -hash BIRKHOFF:def_1_:_ for S being non empty non void ManySortedSign for X being V2() ManySortedSet of the carrier of S for A being non-empty MSAlgebra over S for F being ManySortedFunction of X, the Sorts of A for b5 being ManySortedFunction of (FreeMSA X),A holds ( b5 = F -hash iff ( b5 is_homomorphism FreeMSA X,A & b5 || (FreeGen X) = F ** (Reverse X) ) ); theorem Th1: :: BIRKHOFF:1 for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for X being V2() ManySortedSet of the carrier of S for F being ManySortedFunction of X, the Sorts of A holds rngs F c= rngs (F -hash) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for X being V2() ManySortedSet of the carrier of S for F being ManySortedFunction of X, the Sorts of A holds rngs F c= rngs (F -hash) let A be non-empty MSAlgebra over S; ::_thesis: for X being V2() ManySortedSet of the carrier of S for F being ManySortedFunction of X, the Sorts of A holds rngs F c= rngs (F -hash) let X be V2() ManySortedSet of the carrier of S; ::_thesis: for F being ManySortedFunction of X, the Sorts of A holds rngs F c= rngs (F -hash) let F be ManySortedFunction of X, the Sorts of A; ::_thesis: rngs F c= rngs (F -hash) set R = Reverse X; let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or (rngs F) . i c= (rngs (F -hash)) . i ) assume i in the carrier of S ; ::_thesis: (rngs F) . i c= (rngs (F -hash)) . i then reconsider s = i as SortSymbol of S ; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (rngs F) . i or y in (rngs (F -hash)) . i ) A1: dom ((Reverse X) . 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 by PBOOLE:def_2; assume y in (rngs F) . i ; ::_thesis: y in (rngs (F -hash)) . i then y in rng (F . s) by MSSUBFAM:13; then consider x being set such that A3: x in dom (F . s) and A4: y = (F . s) . x by FUNCT_1:def_3; rngs (Reverse X) = X by EXTENS_1:10; then Reverse X is "onto" by EXTENS_1:9; then rng ((Reverse X) . s) = X . s by MSUALG_3:def_3; then consider a being set such that A5: a in dom ((Reverse X) . s) and A6: x = ((Reverse X) . 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) * ((Reverse X) . s)) . a by A4, A5, A6, FUNCT_1:13 .= ((F ** (Reverse X)) . 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 y in (rngs (F -hash)) . i by MSSUBFAM:13; ::_thesis: verum end; scheme :: BIRKHOFF:sch 1 ExFreeAlg1{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), P1[ set ] } : ex A being strict non-empty MSAlgebra over F1() ex F being ManySortedFunction of F2(),A st ( P1[A] & F is_epimorphism F2(),A & ( for B being non-empty MSAlgebra over F1() for G being ManySortedFunction of F2(),B st G is_homomorphism F2(),B & P1[B] holds ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K ** F = G holds H = K ) ) ) ) provided A1: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds P1[B] and A2: for A being non-empty MSAlgebra over F1() for B being strict non-empty MSSubAlgebra of A st P1[A] holds P1[B] and A3: for I being set for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds ex A being MSAlgebra over F1() st ( A = F . i & P1[A] ) ) holds P1[ product F] proof set EMF = the MSAlgebra-Family of {} ,F1(); set CC = { C where C is Element of (CongrLatt F2()) : ex R being MSCongruence of F2() st ( R = C & P1[ QuotMSAlg (F2(),R)] ) } ; set SF = the Sorts of F2(); set I = the carrier of F1(); consider Xi being ManySortedSet of the carrier of F1() such that A4: {Xi} = the carrier of F1() --> {{}} by MSUALG_9:5; now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_F1()_holds_ the_Sorts_of_(product_the_MSAlgebra-Family_of_{}_,F1())_._i_=_{Xi}_._i let i be set ; ::_thesis: ( i in the carrier of F1() implies the Sorts of (product the MSAlgebra-Family of {} ,F1()) . i = {Xi} . i ) assume i in the carrier of F1() ; ::_thesis: the Sorts of (product the MSAlgebra-Family of {} ,F1()) . i = {Xi} . i then reconsider s = i as SortSymbol of F1() ; thus the Sorts of (product the MSAlgebra-Family of {} ,F1()) . i = product (Carrier ( the MSAlgebra-Family of {} ,F1(),s)) by PRALG_2:def_10 .= {{}} by CARD_3:10, PRALG_2:def_9 .= ( the carrier of F1() --> {{}}) . s by FUNCOP_1:7 .= {Xi} . i by A4 ; ::_thesis: verum end; then A5: the Sorts of (product the MSAlgebra-Family of {} ,F1()) = {Xi} by PBOOLE:3; reconsider R = [| the Sorts of F2(), the Sorts of F2()|] as MSCongruence of F2() by MSUALG_5:18; [| the Sorts of F2(), the Sorts of F2()|] is MSCongruence of F2() by MSUALG_5:18; then A6: [| the Sorts of F2(), the Sorts of F2()|] is Element of (CongrLatt F2()) by MSUALG_5:def_6; the Sorts of (QuotMSAlg (F2(),R)) = { the Sorts of F2()} by MSUALG_9:29; then A7: QuotMSAlg (F2(),R), Trivial_Algebra F1() are_isomorphic by MSUALG_9:26; for i being set st i in {} holds ex A being MSAlgebra over F1() st ( A = the MSAlgebra-Family of {} ,F1() . i & P1[A] ) ; then P1[ product the MSAlgebra-Family of {} ,F1()] by A3; then P1[ Trivial_Algebra F1()] by A1, A5, MSUALG_9:26; then P1[ QuotMSAlg (F2(),R)] by A1, A7, MSUALG_3:17; then A8: [| the Sorts of F2(), the Sorts of F2()|] in { C where C is Element of (CongrLatt F2()) : ex R being MSCongruence of F2() st ( R = C & P1[ QuotMSAlg (F2(),R)] ) } by A6; defpred S1[ set , set ] means ex R being MSCongruence of F2() st ( R = \$1 & \$2 = QuotMSAlg (F2(),R) ); defpred S2[ set ] means ex R being MSCongruence of F2() st ( R = \$1 & P1[ QuotMSAlg (F2(),R)] ); A9: now__::_thesis:_for_q_being_set_st_q_in__{__C_where_C_is_Element_of_(CongrLatt_F2())_:_ex_R_being_MSCongruence_of_F2()_st_ (_R_=_C_&_P1[_QuotMSAlg_(F2(),R)]_)__}__holds_ q_is_MSCongruence_of_F2() let q be set ; ::_thesis: ( q in { C where C is Element of (CongrLatt F2()) : ex R being MSCongruence of F2() st ( R = C & P1[ QuotMSAlg (F2(),R)] ) } implies q is MSCongruence of F2() ) assume q in { C where C is Element of (CongrLatt F2()) : ex R being MSCongruence of F2() st ( R = C & P1[ QuotMSAlg (F2(),R)] ) } ; ::_thesis: q is MSCongruence of F2() then ex C being Element of (CongrLatt F2()) st ( q = C & ex R being MSCongruence of F2() st ( R = C & P1[ QuotMSAlg (F2(),R)] ) ) ; hence q is MSCongruence of F2() ; ::_thesis: verum end; A10: { C where C is Element of (CongrLatt F2()) : ex R being MSCongruence of F2() st ( R = C & P1[ QuotMSAlg (F2(),R)] ) } c= the carrier of (EqRelLatt the Sorts of F2()) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { C where C is Element of (CongrLatt F2()) : ex R being MSCongruence of F2() st ( R = C & P1[ QuotMSAlg (F2(),R)] ) } or q in the carrier of (EqRelLatt the Sorts of F2()) ) assume q in { C where C is Element of (CongrLatt F2()) : ex R being MSCongruence of F2() st ( R = C & P1[ QuotMSAlg (F2(),R)] ) } ; ::_thesis: q in the carrier of (EqRelLatt the Sorts of F2()) then q is Equivalence_Relation of the Sorts of F2() by A9; hence q in the carrier of (EqRelLatt the Sorts of F2()) by MSUALG_5:def_5; ::_thesis: verum end; then reconsider CC = { C where C is Element of (CongrLatt F2()) : ex R being MSCongruence of F2() st ( R = C & P1[ QuotMSAlg (F2(),R)] ) } as non empty SubsetFamily of [| the Sorts of F2(), the Sorts of F2()|] by A8, MSUALG_7:5; set R0 = meet |:CC:|; A11: meet |:CC:| is MSEquivalence_Relation-like ManySortedRelation of the Sorts of F2() by A10, MSUALG_7:8; reconsider R0 = meet |:CC:| as ManySortedRelation of F2() by A10, MSUALG_7:8; R0 is MSEquivalence-like proof let i be set ; :: according to MSUALG_4:def_2,MSUALG_4:def_3 ::_thesis: for b1 being Element of bool [:( the Sorts of F2() . i),( the Sorts of F2() . i):] holds ( not i in the carrier of F1() or not R0 . i = b1 or b1 is Element of bool [:( the Sorts of F2() . i),( the Sorts of F2() . i):] ) let R be Relation of ( the Sorts of F2() . i); ::_thesis: ( not i in the carrier of F1() or not R0 . i = R or R is Element of bool [:( the Sorts of F2() . i),( the Sorts of F2() . i):] ) assume that A12: i in the carrier of F1() and A13: R0 . i = R ; ::_thesis: R is Element of bool [:( the Sorts of F2() . i),( the Sorts of F2() . i):] thus R is Element of bool [:( the Sorts of F2() . i),( the Sorts of F2() . i):] by A11, A12, A13, MSUALG_4:def_2; ::_thesis: verum end; then reconsider R0 = R0 as MSEquivalence-like ManySortedRelation of F2() ; { C where C is Element of (CongrLatt F2()) : S2[C] } is Subset of (CongrLatt F2()) from DOMAIN_1:sch_7(); then reconsider R0 = R0 as MSCongruence of F2() by MSUALG_9:28; take A = QuotMSAlg (F2(),R0); ::_thesis: ex F being ManySortedFunction of F2(),A st ( P1[A] & F is_epimorphism F2(),A & ( for B being non-empty MSAlgebra over F1() for G being ManySortedFunction of F2(),B st G is_homomorphism F2(),B & P1[B] holds ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K ** F = G holds H = K ) ) ) ) reconsider F = MSNat_Hom (F2(),R0) as ManySortedFunction of F2(),A ; take F ; ::_thesis: ( P1[A] & F is_epimorphism F2(),A & ( for B being non-empty MSAlgebra over F1() for G being ManySortedFunction of F2(),B st G is_homomorphism F2(),B & P1[B] holds ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K ** F = G holds H = K ) ) ) ) A14: now__::_thesis:_for_c_being_set_st_c_in_CC_holds_ ex_w_being_set_st_S1[c,w] let c be set ; ::_thesis: ( c in CC implies ex w being set st S1[c,w] ) assume c in CC ; ::_thesis: ex w being set st S1[c,w] then reconsider cc = c as MSCongruence of F2() by A9; consider w being set such that A15: w = QuotMSAlg (F2(),cc) ; take w = w; ::_thesis: S1[c,w] thus S1[c,w] by A15; ::_thesis: verum end; consider FF being ManySortedSet of CC such that A16: for c being set st c in CC holds S1[c,FF . c] from PBOOLE:sch_3(A14); FF is MSAlgebra-Family of CC,F1() proof let c be set ; :: according to PRALG_2:def_5 ::_thesis: ( not c in CC or FF . c is MSAlgebra over F1() ) assume c in CC ; ::_thesis: FF . c is MSAlgebra over F1() then ex R being MSCongruence of F2() st ( R = c & FF . c = QuotMSAlg (F2(),R) ) by A16; hence FF . c is MSAlgebra over F1() ; ::_thesis: verum end; then reconsider FF = FF as MSAlgebra-Family of CC,F1() ; defpred S3[ Element of CC, set ] means ex F1 being ManySortedFunction of F2(),(FF . \$1) st ( F1 = \$2 & F1 is_homomorphism F2(),FF . \$1 & ex R being MSCongruence of F2() st ( \$1 = R & F1 = MSNat_Hom (F2(),R) ) ); A17: for c being Element of CC ex j being set st S3[c,j] proof let c be Element of CC; ::_thesis: ex j being set st S3[c,j] consider R being MSCongruence of F2() such that A18: R = c and A19: FF . c = QuotMSAlg (F2(),R) by A16; set j = MSNat_Hom (F2(),R); reconsider F1 = MSNat_Hom (F2(),R) as ManySortedFunction of F2(),(FF . c) by A19; take MSNat_Hom (F2(),R) ; ::_thesis: S3[c, MSNat_Hom (F2(),R)] take F1 ; ::_thesis: ( F1 = MSNat_Hom (F2(),R) & F1 is_homomorphism F2(),FF . c & ex R being MSCongruence of F2() st ( c = R & F1 = MSNat_Hom (F2(),R) ) ) thus F1 = MSNat_Hom (F2(),R) ; ::_thesis: ( F1 is_homomorphism F2(),FF . c & ex R being MSCongruence of F2() st ( c = R & F1 = MSNat_Hom (F2(),R) ) ) MSNat_Hom (F2(),R) is_epimorphism F2(), QuotMSAlg (F2(),R) by MSUALG_4:3; hence F1 is_homomorphism F2(),FF . c by A19, MSUALG_3:def_8; ::_thesis: ex R being MSCongruence of F2() st ( c = R & F1 = MSNat_Hom (F2(),R) ) take R ; ::_thesis: ( c = R & F1 = MSNat_Hom (F2(),R) ) thus ( c = R & F1 = MSNat_Hom (F2(),R) ) by A18; ::_thesis: verum end; consider FofI1 being ManySortedSet of CC such that A20: for c being Element of CC holds S3[c,FofI1 . c] from PBOOLE:sch_6(A17); A21: for c being Element of CC ex F1 being ManySortedFunction of F2(),(FF . c) st ( F1 = FofI1 . c & F1 is_homomorphism F2(),FF . c ) proof let c be Element of CC; ::_thesis: ex F1 being ManySortedFunction of F2(),(FF . c) st ( F1 = FofI1 . c & F1 is_homomorphism F2(),FF . c ) consider F1 being ManySortedFunction of F2(),(FF . c) such that A22: F1 = FofI1 . c and A23: F1 is_homomorphism F2(),FF . c and ex R being MSCongruence of F2() st ( c = R & F1 = MSNat_Hom (F2(),R) ) by A20; take F1 ; ::_thesis: ( F1 = FofI1 . c & F1 is_homomorphism F2(),FF . c ) thus ( F1 = FofI1 . c & F1 is_homomorphism F2(),FF . c ) by A22, A23; ::_thesis: verum end; FofI1 is Function-yielding proof let c be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not c in dom FofI1 or FofI1 . c is set ) assume c in dom FofI1 ; ::_thesis: FofI1 . c is set then reconsider cc = c as Element of CC ; ex F1 being ManySortedFunction of F2(),(FF . cc) st ( F1 = FofI1 . cc & F1 is_homomorphism F2(),FF . cc ) by A21; hence FofI1 . c is set ; ::_thesis: verum end; then reconsider FofI1 = FofI1 as ManySortedFunction of CC ; consider H being ManySortedFunction of F2(),(product FF) such that A24: H is_homomorphism F2(), product FF and A25: for c being Element of CC holds (proj (FF,c)) ** H = FofI1 . c by A21, PRALG_3:29; now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_F1()_holds_ (MSCng_H)_._i_=_R0_._i let i be set ; ::_thesis: ( i in the carrier of F1() implies (MSCng H) . i = R0 . i ) assume i in the carrier of F1() ; ::_thesis: (MSCng H) . i = R0 . i then reconsider s = i as SortSymbol of F1() ; consider Q being Subset-Family of ([| the Sorts of F2(), the Sorts of F2()|] . s) such that A26: Q = |:CC:| . s and A27: (meet |:CC:|) . s = Intersect Q by MSSUBFAM:def_1; A28: |:CC:| . s = { (t . s) where t is Element of Bool [| the Sorts of F2(), the Sorts of F2()|] : t in CC } by CLOSURE2:14; (MSCng H) . s = R0 . s proof let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in (MSCng H) . s or [a,b] in R0 . s ) & ( not [a,b] in R0 . s or [a,b] in (MSCng H) . s ) ) hereby ::_thesis: ( not [a,b] in R0 . s or [a,b] in (MSCng H) . s ) assume A29: [a,b] in (MSCng H) . s ; ::_thesis: [a,b] in R0 . s then A30: a in the Sorts of F2() . s by ZFMISC_1:87; A31: b in the Sorts of F2() . s by A29, ZFMISC_1:87; A32: [a,b] in MSCng (H,s) by A24, A29, MSUALG_4:def_18; A33: for Y being set st Y in Q holds [a,b] in Y proof let Y be set ; ::_thesis: ( Y in Q implies [a,b] in Y ) assume Y in Q ; ::_thesis: [a,b] in Y then consider t being Element of Bool [| the Sorts of F2(), the Sorts of F2()|] such that A34: Y = t . s and A35: t in CC by A26, A28; reconsider t1 = t as Element of CC by A35; consider F1 being ManySortedFunction of F2(),(FF . t1) such that A36: F1 = FofI1 . t1 and F1 is_homomorphism F2(),FF . t1 and A37: ex R being MSCongruence of F2() st ( t1 = R & F1 = MSNat_Hom (F2(),R) ) by A20; (F1 . s) . a = (((proj (FF,t1)) ** H) . s) . a by A25, A36 .= (((proj (FF,t1)) . s) * (H . s)) . a by MSUALG_3:2 .= ((proj (FF,t1)) . s) . ((H . s) . a) by A30, FUNCT_2:15 .= ((proj (FF,t1)) . s) . ((H . s) . b) by A30, A31, A32, MSUALG_4:def_17 .= (((proj (FF,t1)) . s) * (H . s)) . b by A31, FUNCT_2:15 .= (((proj (FF,t1)) ** H) . s) . b by MSUALG_3:2 .= (F1 . s) . b by A25, A36 ; hence [a,b] in Y by A30, A31, A34, A37, MSUALG_9:33; ::_thesis: verum end; [a,b] in [:( the Sorts of F2() . s),( the Sorts of F2() . s):] by A29; then [a,b] in [| the Sorts of F2(), the Sorts of F2()|] . s by PBOOLE:def_16; hence [a,b] in R0 . s by A27, A33, SETFAM_1:43; ::_thesis: verum end; assume A38: [a,b] in R0 . s ; ::_thesis: [a,b] in (MSCng H) . s then A39: a in the Sorts of F2() . s by ZFMISC_1:87; A40: b in the Sorts of F2() . s by A38, ZFMISC_1:87; A41: for c being 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; ::_thesis: (proj ((Carrier (FF,s)),c)) . ((H . s) . a) = (proj ((Carrier (FF,s)),c)) . ((H . s) . b) reconsider t1 = c as MSCongruence of F2() by A9; consider F1 being ManySortedFunction of F2(),(FF . c) such that A42: F1 = FofI1 . c and F1 is_homomorphism F2(),FF . c and A43: ex R being MSCongruence of F2() st ( c = R & F1 = MSNat_Hom (F2(),R) ) by A20; t1 is Element of Bool [| the Sorts of F2(), the Sorts of F2()|] by CLOSURE2:def_1; then t1 . s in |:CC:| . s by A28; then A44: [a,b] in t1 . s by A26, A27, A38, 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 A39, FUNCT_2:15 .= (((proj (FF,c)) ** H) . s) . a by MSUALG_3:2 .= (F1 . s) . a by A25, A42 .= (F1 . s) . b by A39, A40, A44, A43, MSUALG_9:33 .= (((proj (FF,c)) ** H) . s) . b by A25, A42 .= (((proj (FF,c)) . s) * (H . s)) . b by MSUALG_3:2 .= ((proj (FF,c)) . s) . ((H . s) . b) by A40, FUNCT_2:15 .= (proj ((Carrier (FF,s)),c)) . ((H . s) . b) by PRALG_3:def_2 ; ::_thesis: verum end; (H . s) . b in the Sorts of (product FF) . s by A40, FUNCT_2:5; then A45: (H . s) . b in product (Carrier (FF,s)) by PRALG_2:def_10; (H . s) . a in the Sorts of (product FF) . s by A39, 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 A45, A41, MSUALG_9:14; then [a,b] in MSCng (H,s) by A39, A40, MSUALG_4:def_17; hence [a,b] in (MSCng H) . s by A24, MSUALG_4:def_18; ::_thesis: verum end; hence (MSCng H) . i = R0 . i ; ::_thesis: verum end; then A46: MSCng H = R0 by PBOOLE:3; QuotMSAlg (F2(),(MSCng H)), Image (MSHomQuot H) are_isomorphic by A24, MSUALG_4:4, MSUALG_9:16; then consider XX being strict non-empty MSSubAlgebra of product FF such that A47: A,XX are_isomorphic by A46; for cc being set st cc in CC holds ex A being MSAlgebra over F1() st ( A = FF . cc & P1[A] ) proof let cc be set ; ::_thesis: ( cc in CC implies ex A being MSAlgebra over F1() st ( A = FF . cc & P1[A] ) ) assume A48: cc in CC ; ::_thesis: ex A being MSAlgebra over F1() st ( A = FF . cc & P1[A] ) then reconsider c = cc as Element of CC ; take FF . c ; ::_thesis: ( FF . c = FF . cc & P1[FF . c] ) A49: ex C being Element of (CongrLatt F2()) st ( cc = C & ex R being MSCongruence of F2() st ( R = C & P1[ QuotMSAlg (F2(),R)] ) ) by A48; ex R being MSCongruence of F2() st ( R = cc & FF . cc = QuotMSAlg (F2(),R) ) by A16, A48; hence ( FF . c = FF . cc & P1[FF . c] ) by A49; ::_thesis: verum end; then P1[XX] by A2, A3; hence P1[A] by A1, A47, MSUALG_3:17; ::_thesis: ( F is_epimorphism F2(),A & ( for B being non-empty MSAlgebra over F1() for G being ManySortedFunction of F2(),B st G is_homomorphism F2(),B & P1[B] holds ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K ** F = G holds H = K ) ) ) ) thus F is_epimorphism F2(),A by MSUALG_4:3; ::_thesis: for B being non-empty MSAlgebra over F1() for G being ManySortedFunction of F2(),B st G is_homomorphism F2(),B & P1[B] holds ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K ** F = G holds H = K ) ) then A50: F is "onto" by MSUALG_3:def_8; let B be non-empty MSAlgebra over F1(); ::_thesis: for G being ManySortedFunction of F2(),B st G is_homomorphism F2(),B & P1[B] holds ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K ** F = G holds H = K ) ) let G be ManySortedFunction of F2(),B; ::_thesis: ( G is_homomorphism F2(),B & P1[B] implies ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K ** F = G holds H = K ) ) ) assume that A51: G is_homomorphism F2(),B and A52: P1[B] ; ::_thesis: ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K ** F = G holds H = K ) ) reconsider C = Image (MSHomQuot G) as strict non-empty MSSubAlgebra of B ; A53: QuotMSAlg (F2(),(MSCng G)),C are_isomorphic by A51, MSUALG_4:4, MSUALG_9:16; A54: MSCng G is Element of (CongrLatt F2()) by MSUALG_5:def_6; P1[C] by A2, A52; then P1[ QuotMSAlg (F2(),(MSCng G))] by A1, A53, MSUALG_3:17; then MSCng G in CC by A54; then R0 c= MSCng G by CLOSURE2:21, MSSUBFAM:43; then consider H being ManySortedFunction of A,B such that A55: H is_homomorphism A,B and A56: G = H ** F by A51, MSUALG_9:36; take H ; ::_thesis: ( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K ** F = G holds H = K ) ) thus H is_homomorphism A,B by A55; ::_thesis: ( H ** F = G & ( for K being ManySortedFunction of A,B st K ** F = G holds H = K ) ) thus G = H ** F by A56; ::_thesis: for K being ManySortedFunction of A,B st K ** F = G holds H = K let K be ManySortedFunction of A,B; ::_thesis: ( K ** F = G implies H = K ) assume K ** F = G ; ::_thesis: H = K hence H = K by A56, A50, EXTENS_1:12; ::_thesis: verum end; scheme :: BIRKHOFF:sch 2 ExFreeAlg2{ F1() -> non empty non void ManySortedSign , F2() -> V2() ManySortedSet of the carrier of F1(), P1[ set ] } : ex A being strict non-empty MSAlgebra over F1() ex F being ManySortedFunction of F2(), the Sorts of A st ( P1[A] & ( for B being non-empty MSAlgebra over F1() for G being ManySortedFunction of F2(), the Sorts of B st P1[B] holds ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** F = G holds H = K ) ) ) ) provided A1: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds P1[B] and A2: for A being non-empty MSAlgebra over F1() for B being strict non-empty MSSubAlgebra of A st P1[A] holds P1[B] and A3: for I being set for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds ex A being MSAlgebra over F1() st ( A = F . i & P1[A] ) ) holds P1[ product F] proof A4: for A being non-empty MSAlgebra over F1() for B being strict non-empty MSSubAlgebra of A st P1[A] holds P1[B] by A2; A5: for I being set for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds ex A being MSAlgebra over F1() st ( A = F . i & P1[A] ) ) holds P1[ product F] by A3; set FM = FreeMSA F2(); A6: Reverse F2() is "1-1" by MSUALG_9:11; A7: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds P1[B] by A1; consider A being strict non-empty MSAlgebra over F1(), F being ManySortedFunction of (FreeMSA F2()),A such that A8: P1[A] and A9: F is_epimorphism FreeMSA F2(),A and A10: for B being non-empty MSAlgebra over F1() for G being ManySortedFunction of (FreeMSA F2()),B st G is_homomorphism FreeMSA F2(),B & P1[B] holds ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K ** F = G holds H = K ) ) from BIRKHOFF:sch_1(A7, A4, A5); reconsider R = (F || (FreeGen F2())) ** ((Reverse F2()) "") as ManySortedFunction of F2(), the Sorts of A ; take A ; ::_thesis: ex F being ManySortedFunction of F2(), the Sorts of A st ( P1[A] & ( for B being non-empty MSAlgebra over F1() for G being ManySortedFunction of F2(), the Sorts of B st P1[B] holds ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** F = G holds H = K ) ) ) ) take R ; ::_thesis: ( P1[A] & ( for B being non-empty MSAlgebra over F1() for G being ManySortedFunction of F2(), the Sorts of B st P1[B] holds ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds H = K ) ) ) ) thus P1[A] by A8; ::_thesis: for B being non-empty MSAlgebra over F1() for G being ManySortedFunction of F2(), the Sorts of B st P1[B] holds ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds H = K ) ) let B be non-empty MSAlgebra over F1(); ::_thesis: for G being ManySortedFunction of F2(), the Sorts of B st P1[B] holds ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds H = K ) ) let G be ManySortedFunction of F2(), the Sorts of B; ::_thesis: ( P1[B] implies ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds H = K ) ) ) assume A11: P1[B] ; ::_thesis: ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds H = K ) ) consider GG being ManySortedFunction of (FreeMSA F2()),B such that A12: GG is_homomorphism FreeMSA F2(),B and A13: GG || (FreeGen F2()) = G ** (Reverse F2()) by MSAFREE:def_5; consider H being ManySortedFunction of A,B such that A14: H is_homomorphism A,B and A15: H ** F = GG and for K being ManySortedFunction of A,B st K ** F = GG holds H = K by A10, A11, A12; take H ; ::_thesis: ( H is_homomorphism A,B & H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds H = K ) ) thus H is_homomorphism A,B by A14; ::_thesis: ( H ** R = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds H = K ) ) A16: H ** (F || (FreeGen F2())) = GG || (FreeGen F2()) by A15, EXTENS_1:4; A17: F is "onto" by A9, MSUALG_3:def_8; rngs (Reverse F2()) = F2() by EXTENS_1:10; then A18: Reverse F2() is "onto" by EXTENS_1:9; R ** (Reverse F2()) = (F || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2())) by PBOOLE:140 .= (F || (FreeGen F2())) ** (id (FreeGen F2())) by A18, A6, MSUALG_3:5 .= F || (FreeGen F2()) by MSUALG_3:3 ; then A19: (H ** R) ** (Reverse F2()) = G ** (Reverse F2()) by A13, A16, PBOOLE:140; hence H ** R = G by A18, EXTENS_1:12; ::_thesis: for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** R = G holds H = K let K be ManySortedFunction of A,B; ::_thesis: ( K is_homomorphism A,B & K ** R = G implies H = K ) assume A20: K is_homomorphism A,B ; ::_thesis: ( not K ** R = G or H = K ) assume K ** R = G ; ::_thesis: H = K then K ** (((F || (FreeGen F2())) ** ((Reverse F2()) "")) ** (Reverse F2())) = (H ** ((F || (FreeGen F2())) ** ((Reverse F2()) ""))) ** (Reverse F2()) by A19, PBOOLE:140; then K ** (((F || (FreeGen F2())) ** ((Reverse F2()) "")) ** (Reverse F2())) = H ** (((F || (FreeGen F2())) ** ((Reverse F2()) "")) ** (Reverse F2())) by PBOOLE:140; then K ** ((F || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2()))) = H ** (((F || (FreeGen F2())) ** ((Reverse F2()) "")) ** (Reverse F2())) by PBOOLE:140; then K ** ((F || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2()))) = H ** ((F || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2()))) by PBOOLE:140; then K ** ((F || (FreeGen F2())) ** (id (FreeGen F2()))) = H ** ((F || (FreeGen F2())) ** (((Reverse F2()) "") ** (Reverse F2()))) by A18, A6, MSUALG_3:5; then K ** ((F || (FreeGen F2())) ** (id (FreeGen F2()))) = H ** ((F || (FreeGen F2())) ** (id (FreeGen F2()))) by A18, A6, MSUALG_3:5; then K ** (F || (FreeGen F2())) = H ** ((F || (FreeGen F2())) ** (id (FreeGen F2()))) by MSUALG_3:3; then K ** (F || (FreeGen F2())) = H ** (F || (FreeGen F2())) by MSUALG_3:3; then (K ** F) || (FreeGen F2()) = H ** (F || (FreeGen F2())) by EXTENS_1:4; then A21: (K ** F) || (FreeGen F2()) = (H ** F) || (FreeGen F2()) by EXTENS_1:4; F is_homomorphism FreeMSA F2(),A by A9, MSUALG_3:def_8; then K ** F is_homomorphism FreeMSA F2(),B by A20, MSUALG_3:10; then K ** F = H ** F by A12, A15, A21, EXTENS_1:14; hence H = K by A17, EXTENS_1:12; ::_thesis: verum end; scheme :: BIRKHOFF:sch 3 Exhash{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3() -> non-empty MSAlgebra over F1(), F4() -> ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2(), F5() -> ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F3(), P1[ set ] } : ex H being ManySortedFunction of F2(),F3() st ( H is_homomorphism F2(),F3() & F5() -hash = H ** (F4() -hash) ) provided A1: P1[F3()] and A2: for C being non-empty MSAlgebra over F1() for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P1[C] holds ex h being ManySortedFunction of F2(),C st ( h is_homomorphism F2(),C & G = h ** F4() ) proof consider H being ManySortedFunction of F2(),F3() such that A3: H is_homomorphism F2(),F3() and A4: F5() = H ** F4() by A1, A2; take H ; ::_thesis: ( H is_homomorphism F2(),F3() & F5() -hash = H ** (F4() -hash) ) thus H is_homomorphism F2(),F3() by A3; ::_thesis: F5() -hash = H ** (F4() -hash) F4() -hash is_homomorphism FreeMSA ( the carrier of F1() --> NAT),F2() by Def1; then A5: H ** (F4() -hash) is_homomorphism FreeMSA ( the carrier of F1() --> NAT),F3() by A3, MSUALG_3:10; reconsider SN = the carrier of F1() --> NAT as V2() ManySortedSet of the carrier of F1() ; reconsider h1 = F5() as ManySortedFunction of SN, the Sorts of F3() ; A6: h1 -hash is_homomorphism FreeMSA SN,F3() by Def1; (h1 -hash) || (FreeGen SN) = F5() ** (Reverse SN) by Def1 .= H ** (F4() ** (Reverse SN)) by A4, PBOOLE:140 .= H ** ((F4() -hash) || (FreeGen ( the carrier of F1() --> NAT))) by Def1 .= (H ** (F4() -hash)) || (FreeGen ( the carrier of F1() --> NAT)) by EXTENS_1:4 ; hence F5() -hash = H ** (F4() -hash) by A6, A5, EXTENS_1:14; ::_thesis: verum end; scheme :: BIRKHOFF:sch 4 EqTerms{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3() -> ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2(), F4() -> SortSymbol of F1(), F5() -> Element of the Sorts of (TermAlg F1()) . F4(), F6() -> Element of the Sorts of (TermAlg F1()) . F4(), P1[ set ] } : for B being non-empty MSAlgebra over F1() st P1[B] holds B |= F5() '=' F6() provided A1: ((F3() -hash) . F4()) . F5() = ((F3() -hash) . F4()) . F6() and A2: for C being non-empty MSAlgebra over F1() for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P1[C] holds ex h being ManySortedFunction of F2(),C st ( h is_homomorphism F2(),C & G = h ** F3() ) proof reconsider fi1 = F3() as ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2() ; reconsider SN = the carrier of F1() --> NAT as V2() ManySortedSet of the carrier of F1() ; let B be non-empty MSAlgebra over F1(); ::_thesis: ( P1[B] implies B |= F5() '=' F6() ) assume P1[B] ; ::_thesis: B |= F5() '=' F6() then A3: P1[B] ; let h be ManySortedFunction of (TermAlg F1()),B; :: according to EQUATION:def_5 ::_thesis: ( not h is_homomorphism TermAlg F1(),B or (h . F4()) . ((F5() '=' F6()) `1) = (h . F4()) . ((F5() '=' F6()) `2) ) assume A4: h is_homomorphism TermAlg F1(),B ; ::_thesis: (h . F4()) . ((F5() '=' F6()) `1) = (h . F4()) . ((F5() '=' F6()) `2) reconsider h1 = h as ManySortedFunction of (FreeMSA SN),B ; set alfa = (h1 || (FreeGen SN)) ** ((Reverse SN) ""); A5: ((h1 || (FreeGen SN)) ** ((Reverse SN) "")) -hash is_homomorphism FreeMSA SN,B by Def1; reconsider alfa1 = (h1 || (FreeGen SN)) ** ((Reverse SN) "") as ManySortedFunction of the carrier of F1() --> NAT, the Sorts of B ; A6: for C being non-empty MSAlgebra over F1() for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P1[C] holds ex h being ManySortedFunction of F2(),C st ( h is_homomorphism F2(),C & G = h ** fi1 ) by A2; consider H being ManySortedFunction of F2(),B such that H is_homomorphism F2(),B and A7: alfa1 -hash = H ** (fi1 -hash) from BIRKHOFF:sch_3(A3, A6); A8: ((((h1 || (FreeGen SN)) ** ((Reverse SN) "")) -hash) . F4()) . F5() = ((H . F4()) * ((F3() -hash) . F4())) . F5() by A7, MSUALG_3:2 .= (H . F4()) . (((F3() -hash) . F4()) . F6()) by A1, FUNCT_2:15 .= ((H . F4()) * ((F3() -hash) . F4())) . F6() by FUNCT_2:15 .= ((((h1 || (FreeGen SN)) ** ((Reverse SN) "")) -hash) . F4()) . F6() by A7, MSUALG_3:2 ; rngs (Reverse SN) = SN by EXTENS_1:10; then A9: ( Reverse SN is "1-1" & Reverse SN is "onto" ) by EXTENS_1:9, MSUALG_9:11; (((h1 || (FreeGen SN)) ** ((Reverse SN) "")) -hash) || (FreeGen SN) = ((h1 || (FreeGen SN)) ** ((Reverse SN) "")) ** (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: ((h1 || (FreeGen SN)) ** ((Reverse SN) "")) -hash = h1 by A4, A5, EXTENS_1:14; thus (h . F4()) . ([F5(),F6()] `1) = (h . F4()) . F5() .= (h . F4()) . ([F5(),F6()] `2) by A10, A8 ; ::_thesis: verum end; scheme :: BIRKHOFF:sch 5 FreeIsGen{ F1() -> non empty non void ManySortedSign , F2() -> V2() ManySortedSet of the carrier of F1(), F3() -> strict non-empty MSAlgebra over F1(), F4() -> ManySortedFunction of F2(), the Sorts of F3(), P1[ set ] } : F4() .:.: F2() is V2() GeneratorSet of F3() provided A1: for C being non-empty MSAlgebra over F1() for G being ManySortedFunction of F2(), the Sorts of C st P1[C] holds ex H being ManySortedFunction of F3(),C st ( H is_homomorphism F3(),C & H ** F4() = G & ( for K being ManySortedFunction of F3(),C st K is_homomorphism F3(),C & K ** F4() = G holds H = K ) ) and A2: P1[F3()] and A3: for A being non-empty MSAlgebra over F1() for B being strict non-empty MSSubAlgebra of A st P1[A] holds P1[B] proof set I = the carrier of F1(); A4: F4() .:.: F2() is V2() proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in the carrier of F1() or not (F4() .:.: F2()) . i is empty ) assume A5: i in the carrier of F1() ; ::_thesis: not (F4() .:.: F2()) . i is empty then reconsider fi = F4() . i as Function of (F2() . i),( the Sorts of F3() . i) by PBOOLE:def_15; A6: (F4() .:.: F2()) . i = fi .: (F2() . i) by A5, PBOOLE:def_20; reconsider Xi = F2() . i as non empty set by A5; A7: Xi meets Xi ; dom fi = Xi by A5, FUNCT_2:def_1; hence not (F4() .:.: F2()) . i is empty by A7, A6, RELAT_1:118; ::_thesis: verum end; F4() .:.: F2() is ManySortedSubset of the Sorts of F3() proof let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in the carrier of F1() or (F4() .:.: F2()) . i c= the Sorts of F3() . i ) assume A8: i in the carrier of F1() ; ::_thesis: (F4() .:.: F2()) . i c= the Sorts of F3() . i then reconsider fi = F4() . i as Function of (F2() . i),( the Sorts of F3() . i) by PBOOLE:def_15; (F4() .:.: F2()) . i = fi .: (F2() . i) by A8, PBOOLE:def_20; hence (F4() .:.: F2()) . i c= the Sorts of F3() . i ; ::_thesis: verum end; then reconsider Gen = F4() .:.: F2() as V2() MSSubset of F3() by A4; set AA = GenMSAlg Gen; A9: F2() is_transformable_to the Sorts of (GenMSAlg Gen) proof let i be set ; :: according to PZFMISC1:def_3 ::_thesis: ( not i in the carrier of F1() or not the Sorts of (GenMSAlg Gen) . i = {} or F2() . i = {} ) assume i in the carrier of F1() ; ::_thesis: ( not the Sorts of (GenMSAlg Gen) . i = {} or F2() . i = {} ) hence ( not the Sorts of (GenMSAlg Gen) . i = {} or F2() . i = {} ) ; ::_thesis: verum end; F2() is_transformable_to the Sorts of F3() proof let i be set ; :: according to PZFMISC1:def_3 ::_thesis: ( not i in the carrier of F1() or not the Sorts of F3() . i = {} or F2() . i = {} ) assume i in the carrier of F1() ; ::_thesis: ( not the Sorts of F3() . i = {} or F2() . i = {} ) hence ( not the Sorts of F3() . i = {} or F2() . i = {} ) ; ::_thesis: verum end; then A10: doms F4() = F2() by MSSUBFAM:17; then rngs F4() = F4() .:.: F2() by EQUATION:13; then rngs F4() is ManySortedSubset of the Sorts of (GenMSAlg Gen) by MSUALG_2:def_17; then rngs F4() c= the Sorts of (GenMSAlg Gen) by PBOOLE:def_18; then reconsider iN = F4() as ManySortedFunction of F2(), the Sorts of (GenMSAlg Gen) by A9, A10, EQUATION:4; consider IN being ManySortedFunction of F3(),(GenMSAlg Gen) such that A11: IN is_homomorphism F3(), GenMSAlg Gen and A12: IN ** F4() = iN and for K being ManySortedFunction of F3(),(GenMSAlg Gen) st K is_homomorphism F3(), GenMSAlg Gen & K ** F4() = iN holds IN = K by A1, A2, A3; the Sorts of (GenMSAlg Gen) is ManySortedSubset of the Sorts of F3() by MSUALG_2:def_9; then reconsider h = id the Sorts of (GenMSAlg Gen) as ManySortedFunction of (GenMSAlg Gen),F3() by EXTENS_1:5; consider HIN being ManySortedFunction of F3(),F3() such that HIN is_homomorphism F3(),F3() and HIN ** F4() = h ** iN and A13: for K being ManySortedFunction of F3(),F3() st K is_homomorphism F3(),F3() & K ** F4() = h ** iN holds HIN = K by A1, A2; h is_monomorphism GenMSAlg Gen,F3() by MSUALG_3:22; then A14: h is_homomorphism GenMSAlg Gen,F3() by MSUALG_3:def_9; reconsider hIN = h ** IN as ManySortedFunction of F3(),F3() ; h ** iN = (h ** IN) ** F4() by A12, PBOOLE:140; then A15: HIN = hIN by A11, A13, A14, MSUALG_3:10; A16: F3() is MSSubAlgebra of F3() by MSUALG_2:5; F4() = h ** iN by MSUALG_3:4; then (id the Sorts of F3()) ** F4() = h ** iN by MSUALG_3:4; then HIN = id the Sorts of F3() by A13, MSUALG_3:9; then A17: HIN is "onto" ; the Sorts of (GenMSAlg Gen) = h .:.: the Sorts of (GenMSAlg Gen) by EQUATION:15 .= the Sorts of F3() by A15, A17, EQUATION:2, EQUATION:9 ; then GenMSAlg Gen = F3() by A16, MSUALG_2:9; hence F4() .:.: F2() is V2() GeneratorSet of F3() by MSAFREE:3; ::_thesis: verum end; scheme :: BIRKHOFF:sch 6 Hashisonto{ F1() -> non empty non void ManySortedSign , F2() -> strict non-empty MSAlgebra over F1(), F3() -> ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2(), P1[ set ] } : F3() -hash is_epimorphism FreeMSA ( the carrier of F1() --> NAT),F2() provided A1: for C being non-empty MSAlgebra over F1() for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P1[C] holds ex H being ManySortedFunction of F2(),C st ( H is_homomorphism F2(),C & H ** F3() = G & ( for K being ManySortedFunction of F2(),C st K is_homomorphism F2(),C & K ** F3() = G holds H = K ) ) and A2: P1[F2()] and A3: for A being non-empty MSAlgebra over F1() for B being strict non-empty MSSubAlgebra of A st P1[A] holds P1[B] proof A4: P1[F2()] by A2; set V = the carrier of F1() --> NAT; reconsider Gen = the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) as GeneratorSet of FreeMSA ( the carrier of F1() --> NAT) by MSAFREE2:6; A5: F3() .:.: ( the carrier of F1() --> NAT) c= rngs F3() by EQUATION:12; the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) is_transformable_to the Sorts of F2() proof let i be set ; :: according to PZFMISC1:def_3 ::_thesis: ( not i in the carrier of F1() or not the Sorts of F2() . i = {} or the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . i = {} ) assume A6: i in the carrier of F1() ; ::_thesis: ( not the Sorts of F2() . i = {} or the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . i = {} ) assume the Sorts of F2() . i = {} ; ::_thesis: the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . i = {} hence the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) . i = {} by A6; ::_thesis: verum end; then doms (F3() -hash) = the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) by MSSUBFAM:17; then A7: (F3() -hash) .:.: the Sorts of (FreeMSA ( the carrier of F1() --> NAT)) = rngs (F3() -hash) by EQUATION:13; rngs F3() c= rngs (F3() -hash) by Th1; then A8: F3() .:.: ( the carrier of F1() --> NAT) c= (F3() -hash) .:.: Gen by A7, A5, PBOOLE:13; A9: F3() -hash is_homomorphism FreeMSA ( the carrier of F1() --> NAT),F2() by Def1; A10: for A being non-empty MSAlgebra over F1() for B being strict non-empty MSSubAlgebra of A st P1[A] holds P1[B] by A3; A11: for C being non-empty MSAlgebra over F1() for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P1[C] holds ex H being ManySortedFunction of F2(),C st ( H is_homomorphism F2(),C & H ** F3() = G & ( for K being ManySortedFunction of F2(),C st K is_homomorphism F2(),C & K ** F3() = G holds H = K ) ) by A1; F3() .:.: ( the carrier of F1() --> NAT) is V2() GeneratorSet of F2() from BIRKHOFF:sch_5(A11, A4, A10); hence F3() -hash is_epimorphism FreeMSA ( the carrier of F1() --> NAT),F2() by A8, A9, EQUATION:23; ::_thesis: verum end; scheme :: BIRKHOFF:sch 7 FinGenAlgInVar{ F1() -> non empty non void ManySortedSign , F2() -> strict non-empty finitely-generated MSAlgebra over F1(), F3() -> non-empty MSAlgebra over F1(), F4() -> ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F3(), P1[ set ], P2[ set ] } : P1[F2()] provided A1: P2[F2()] and A2: P1[F3()] and A3: for C being non-empty MSAlgebra over F1() for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P2[C] holds ex h being ManySortedFunction of F3(),C st ( h is_homomorphism F3(),C & G = h ** F4() ) and A4: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds P1[B] and A5: for A being non-empty MSAlgebra over F1() for R being MSCongruence of A st P1[A] holds P1[ QuotMSAlg (A,R)] proof set I = the carrier of F1(); set sA = the Sorts of F2(); consider Gen being GeneratorSet of F2() such that A6: Gen is V42() by MSAFREE2:def_10; reconsider Gen = Gen as V42() ManySortedSubset of the Sorts of F2() by A6; consider GEN being V2() V42() ManySortedSubset of the Sorts of F2() such that A7: Gen c= GEN by MSUALG_9:7; consider F being ManySortedFunction of the carrier of F1() --> NAT,GEN such that A8: F is "onto" by MSUALG_9:12; the carrier of F1() --> NAT is_transformable_to GEN proof let i be set ; :: according to PZFMISC1:def_3 ::_thesis: ( not i in the carrier of F1() or not GEN . i = {} or ( the carrier of F1() --> NAT) . i = {} ) assume i in the carrier of F1() ; ::_thesis: ( not GEN . i = {} or ( the carrier of F1() --> NAT) . i = {} ) hence ( not GEN . i = {} or ( the carrier of F1() --> NAT) . i = {} ) ; ::_thesis: verum end; then reconsider G = F as ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2() by EXTENS_1:5; consider h being ManySortedFunction of F3(),F2() such that A9: h is_homomorphism F3(),F2() and A10: G = h ** F4() by A1, A3; reconsider sI1 = the Sorts of (Image h) as MSSubset of (Image h) by PBOOLE:def_18; A11: GEN is GeneratorSet of F2() by A7, MSSCYC_1:21; reconsider sI = the Sorts of (Image h) as MSSubset of F2() by MSUALG_2:def_9; GEN is ManySortedSubset of sI proof let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in the carrier of F1() or GEN . i c= sI . i ) assume i in the carrier of F1() ; ::_thesis: GEN . i c= sI . i then reconsider s = i as SortSymbol of F1() ; let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in GEN . i or g in sI . i ) assume A12: g in GEN . i ; ::_thesis: g in sI . i A13: ( the carrier of F1() --> NAT) . s = NAT by FUNCOP_1:7; then reconsider fi = F4() . s as Function of NAT,( the Sorts of F3() . 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 being set 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 A13, 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 F3() . s) by A17, A14, FUNCT_1:def_6; then g in (h .:.: the Sorts of F3()) . s by PBOOLE:def_20; hence g in sI . i by A9, MSUALG_3:def_12; ::_thesis: verum 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 F2() is MSSubAlgebra of Image h by A11, MSAFREE:3; then F2() = Image h by MSUALG_2:7; then A19: h is_epimorphism F3(),F2() by A9, MSUALG_3:19; P1[ QuotMSAlg (F3(),(MSCng h))] by A2, A5; hence P1[F2()] by A4, A19, MSUALG_4:6; ::_thesis: verum end; scheme :: BIRKHOFF:sch 8 QuotEpi{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3() -> non-empty MSAlgebra over F1(), P1[ set ] } : P1[F3()] provided A1: ex H being ManySortedFunction of F2(),F3() st H is_epimorphism F2(),F3() and A2: P1[F2()] and A3: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds P1[B] and A4: for A being non-empty MSAlgebra over F1() for R being MSCongruence of A st P1[A] holds P1[ QuotMSAlg (A,R)] proof consider H being ManySortedFunction of F2(),F3() such that A5: H is_epimorphism F2(),F3() by A1; P1[ QuotMSAlg (F2(),(MSCng H))] by A2, A4; hence P1[F3()] by A3, A5, MSUALG_4:6; ::_thesis: verum end; scheme :: BIRKHOFF:sch 9 AllFinGen{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), P1[ set ] } : P1[F2()] provided A1: for B being strict non-empty finitely-generated MSSubAlgebra of F2() holds P1[B] and A2: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds P1[B] and A3: for A being non-empty MSAlgebra over F1() for B being strict non-empty MSSubAlgebra of A st P1[A] holds P1[B] and A4: for A being non-empty MSAlgebra over F1() for R being MSCongruence of A st P1[A] holds P1[ QuotMSAlg (A,R)] and A5: for I being set for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds ex A being MSAlgebra over F1() st ( A = F . i & P1[A] ) ) holds P1[ product F] proof A6: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds P1[B] by A2; set T = the strict non-empty finitely-generated MSSubAlgebra of F2(); set CC = { C where C is Element of MSSub F2() : ex R being strict non-empty finitely-generated MSSubAlgebra of F2() st R = C } ; the strict non-empty finitely-generated MSSubAlgebra of F2() in MSSub F2() by MSUALG_2:def_19; then the strict non-empty finitely-generated MSSubAlgebra of F2() in { C where C is Element of MSSub F2() : ex R being strict non-empty finitely-generated MSSubAlgebra of F2() st R = C } ; then reconsider CC = { C where C is Element of MSSub F2() : ex R being strict non-empty finitely-generated MSSubAlgebra of F2() st R = C } as non empty set ; defpred S1[ set , set ] means \$1 = \$2; A7: for c being set st c in CC holds ex j being set st S1[c,j] ; consider FF being ManySortedSet of CC such that A8: for c being set st c in CC holds S1[c,FF . c] from PBOOLE:sch_3(A7); FF is MSAlgebra-Family of CC,F1() proof let c be set ; :: according to PRALG_2:def_5 ::_thesis: ( not c in CC or FF . c is MSAlgebra over F1() ) assume A9: c in CC ; ::_thesis: FF . c is MSAlgebra over F1() then ex Q being Element of MSSub F2() st ( c = Q & ex R being strict non-empty finitely-generated MSSubAlgebra of F2() st R = Q ) ; hence FF . c is MSAlgebra over F1() by A8, A9; ::_thesis: verum end; then reconsider FF = FF as MSAlgebra-Family of CC,F1() ; consider prSOR being strict non-empty MSSubAlgebra of product FF such that A10: ex BA being ManySortedFunction of prSOR,F2() st BA is_epimorphism prSOR,F2() by A8, EQUATION:27; A11: for A being non-empty MSAlgebra over F1() for R being MSCongruence of A st P1[A] holds P1[ QuotMSAlg (A,R)] by A4; for i being set st i in CC holds ex A being MSAlgebra over F1() st ( A = FF . i & P1[A] ) proof let i be set ; ::_thesis: ( i in CC implies ex A being MSAlgebra over F1() st ( A = FF . i & P1[A] ) ) assume A12: i in CC ; ::_thesis: ex A being MSAlgebra over F1() st ( A = FF . i & P1[A] ) then consider Q being Element of MSSub F2() such that A13: i = Q and A14: ex R being strict non-empty finitely-generated MSSubAlgebra of F2() st R = Q ; consider R being strict non-empty finitely-generated MSSubAlgebra of F2() such that A15: R = Q by A14; take R ; ::_thesis: ( R = FF . i & P1[R] ) thus ( R = FF . i & P1[R] ) by A1, A8, A12, A13, A15; ::_thesis: verum end; then A16: P1[prSOR] by A3, A5; thus P1[F2()] from BIRKHOFF:sch_8(A10, A16, A6, A11); ::_thesis: verum end; scheme :: BIRKHOFF:sch 10 FreeInModIsInVar1{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), P1[ set ], P2[ set ] } : P2[F2()] provided A1: for A being non-empty MSAlgebra over F1() holds ( P2[A] iff for s being SortSymbol of F1() for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra over F1() st P1[B] holds B |= e ) holds A |= e ) and A2: P1[F2()] proof for s being SortSymbol of F1() for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra over F1() st P1[B] holds B |= e ) holds F2() |= e by A2; hence P2[F2()] by A1; ::_thesis: verum end; scheme :: BIRKHOFF:sch 11 FreeInModIsInVar{ F1() -> non empty non void ManySortedSign , F2() -> strict non-empty MSAlgebra over F1(), F3() -> ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2(), P1[ set ], P2[ set ] } : P1[F2()] provided A1: for A being non-empty MSAlgebra over F1() holds ( P2[A] iff for s being SortSymbol of F1() for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra over F1() st P1[B] holds B |= e ) holds A |= e ) and A2: for C being non-empty MSAlgebra over F1() for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P2[C] holds ex H being ManySortedFunction of F2(),C st ( H is_homomorphism F2(),C & H ** F3() = G & ( for K being ManySortedFunction of F2(),C st K is_homomorphism F2(),C & K ** F3() = G holds H = K ) ) and A3: P2[F2()] and A4: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds P1[B] and A5: for A being non-empty MSAlgebra over F1() for B being strict non-empty MSSubAlgebra of A st P1[A] holds P1[B] and A6: for I being set for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds ex A being MSAlgebra over F1() st ( A = F . i & P1[A] ) ) holds P1[ product F] proof A7: for I being set for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds ex A being MSAlgebra over F1() st ( A = F . i & P1[A] ) ) holds P1[ product F] by A6; set V = the carrier of F1() --> NAT; A8: for A being non-empty MSAlgebra over F1() for B being strict non-empty MSSubAlgebra of A st P1[A] holds P1[B] by A5; A9: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds P1[B] by A4; consider A being strict non-empty MSAlgebra over F1(), fi being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of A such that A10: P1[A] and A11: for B being non-empty MSAlgebra over F1() for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of B st P1[B] holds ex H being ManySortedFunction of A,B st ( H is_homomorphism A,B & H ** fi = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** fi = G holds H = K ) ) from BIRKHOFF:sch_2(A9, A8, A7); A12: for C being non-empty MSAlgebra over F1() for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P2[C] holds ex H being ManySortedFunction of F2(),C st ( H is_homomorphism F2(),C & H ** F3() = G & ( for K being ManySortedFunction of F2(),C st K is_homomorphism F2(),C & K ** F3() = G holds H = K ) ) by A2; A13: for C being non-empty MSAlgebra over F1() for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P2[C] holds ex h being ManySortedFunction of F2(),C st ( h is_homomorphism F2(),C & G = h ** F3() ) proof let C be non-empty MSAlgebra over F1(); ::_thesis: for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P2[C] holds ex h being ManySortedFunction of F2(),C st ( h is_homomorphism F2(),C & G = h ** F3() ) let G be ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C; ::_thesis: ( P2[C] implies ex h being ManySortedFunction of F2(),C st ( h is_homomorphism F2(),C & G = h ** F3() ) ) assume P2[C] ; ::_thesis: ex h being ManySortedFunction of F2(),C st ( h is_homomorphism F2(),C & G = h ** F3() ) then consider h being ManySortedFunction of F2(),C such that A14: h is_homomorphism F2(),C and A15: G = h ** F3() and for K being ManySortedFunction of F2(),C st K is_homomorphism F2(),C & K ** F3() = G holds h = K by A2; take h ; ::_thesis: ( h is_homomorphism F2(),C & G = h ** F3() ) thus ( h is_homomorphism F2(),C & G = h ** F3() ) by A14, A15; ::_thesis: verum end; A16: P2[F2()] by A3; A17: for A being non-empty MSAlgebra over F1() holds ( P2[A] iff for s being SortSymbol of F1() for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra over F1() st P1[B] holds B |= e ) holds A |= e ) by A1; A18: P2[A] from BIRKHOFF:sch_10(A17, A10); consider H being ManySortedFunction of F2(),A such that A19: H is_homomorphism F2(),A and A20: fi -hash = H ** (F3() -hash) from BIRKHOFF:sch_3(A18, A13); A21: F3() -hash is_homomorphism FreeMSA ( the carrier of F1() --> NAT),F2() by Def1; now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_F1()_holds_ H_._i_is_one-to-one let i be set ; ::_thesis: ( i in the carrier of F1() implies H . i is one-to-one ) assume i in the carrier of F1() ; ::_thesis: H . i is one-to-one then reconsider s = i as SortSymbol of F1() ; thus H . i is one-to-one ::_thesis: verum proof A22: for D being non-empty MSAlgebra over F1() for E being strict non-empty MSSubAlgebra of D st P2[D] holds P2[E] proof let D be non-empty MSAlgebra over F1(); ::_thesis: for E being strict non-empty MSSubAlgebra of D st P2[D] holds P2[E] let E be strict non-empty MSSubAlgebra of D; ::_thesis: ( P2[D] implies P2[E] ) assume A23: P2[D] ; ::_thesis: P2[E] now__::_thesis:_for_s_being_SortSymbol_of_F1() for_e_being_Element_of_(Equations_F1())_._s_st_(_for_B_being_non-empty_MSAlgebra_over_F1()_st_P1[B]_holds_ B_|=_e_)_holds_ E_|=_e let s be SortSymbol of F1(); ::_thesis: for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra over F1() st P1[B] holds B |= e ) holds E |= e let e be Element of (Equations F1()) . s; ::_thesis: ( ( for B being non-empty MSAlgebra over F1() st P1[B] holds B |= e ) implies E |= e ) assume for B being non-empty MSAlgebra over F1() st P1[B] holds B |= e ; ::_thesis: E |= e then D |= e by A1, A23; hence E |= e by EQUATION:31; ::_thesis: verum end; hence P2[E] by A1; ::_thesis: verum end; F3() -hash is_epimorphism FreeMSA ( the carrier of F1() --> NAT),F2() from BIRKHOFF:sch_6(A12, A16, A22); then A24: F3() -hash is "onto" by MSUALG_3:def_8; A25: for C being non-empty MSAlgebra over F1() for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P1[C] holds ex H being ManySortedFunction of A,C st ( H is_homomorphism A,C & G = H ** fi ) proof let C be non-empty MSAlgebra over F1(); ::_thesis: for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P1[C] holds ex H being ManySortedFunction of A,C st ( H is_homomorphism A,C & G = H ** fi ) let G be ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C; ::_thesis: ( P1[C] implies ex H being ManySortedFunction of A,C st ( H is_homomorphism A,C & G = H ** fi ) ) assume P1[C] ; ::_thesis: ex H being ManySortedFunction of A,C st ( H is_homomorphism A,C & G = H ** fi ) then consider H being ManySortedFunction of A,C such that A26: H is_homomorphism A,C and A27: H ** fi = G and for K being ManySortedFunction of A,C st K is_homomorphism A,C & K ** fi = G holds H = K by A11; take H ; ::_thesis: ( H is_homomorphism A,C & G = H ** fi ) thus ( H is_homomorphism A,C & G = H ** fi ) by A26, A27; ::_thesis: verum end; let a, b be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a in dom (H . i) or not b in dom (H . i) or not (H . i) . a = (H . i) . b or a = b ) assume that A28: a in dom (H . i) and A29: b in dom (H . i) and A30: (H . i) . a = (H . i) . b ; ::_thesis: a = b A31: dom (H . s) = the Sorts of F2() . s by FUNCT_2:def_1 .= rng ((F3() -hash) . s) by A24, MSUALG_3:def_3 ; then consider t1 being set such that A32: t1 in dom ((F3() -hash) . s) and A33: ((F3() -hash) . s) . t1 = a by A28, FUNCT_1:def_3; consider t2 being set such that A34: t2 in dom ((F3() -hash) . s) and A35: ((F3() -hash) . s) . t2 = b by A29, A31, FUNCT_1:def_3; reconsider t1 = t1, t2 = t2 as Element of the Sorts of (TermAlg F1()) . s by A32, A34; set e = t1 '=' t2; A36: ((fi -hash) . s) . t1 = ((H . s) * ((F3() -hash) . s)) . t1 by A20, MSUALG_3:2 .= (H . s) . a by A33, FUNCT_2:15 .= ((H . s) * ((F3() -hash) . s)) . t2 by A30, A35, FUNCT_2:15 .= ((fi -hash) . s) . t2 by A20, MSUALG_3:2 ; for B being non-empty MSAlgebra over F1() st P1[B] holds B |= t1 '=' t2 from BIRKHOFF:sch_4(A36, A25); then A37: F2() |= t1 '=' t2 by A1, A3; thus a = ((F3() -hash) . s) . ((t1 '=' t2) `1) by A33 .= ((F3() -hash) . s) . ((t1 '=' t2) `2) by A21, A37, EQUATION:def_5 .= b by A35 ; ::_thesis: verum end; end; then H is "1-1" by MSUALG_3:1; then H is_monomorphism F2(),A by A19, MSUALG_3:def_9; then A38: F2(), Image H are_isomorphic by MSUALG_9:16; P1[ Image H] by A5, A10; hence P1[F2()] by A4, A38, MSUALG_3:17; ::_thesis: verum end; scheme :: BIRKHOFF:sch 12 Birkhoff{ F1() -> non empty non void ManySortedSign , P1[ set ] } : ex E being EqualSet of F1() st for A being non-empty MSAlgebra over F1() holds ( P1[A] iff A |= E ) provided A1: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds P1[B] and A2: for A being non-empty MSAlgebra over F1() for B being strict non-empty MSSubAlgebra of A st P1[A] holds P1[B] and A3: for A being non-empty MSAlgebra over F1() for R being MSCongruence of A st P1[A] holds P1[ QuotMSAlg (A,R)] and A4: for I being set for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds ex A being MSAlgebra over F1() st ( A = F . i & P1[A] ) ) holds P1[ product F] proof A5: for A being non-empty MSAlgebra over F1() for B being strict non-empty MSSubAlgebra of A st P1[A] holds P1[B] by A2; set XX = the carrier of F1() --> NAT; set I = the carrier of F1(); defpred S1[ set , set ] means ex s being SortSymbol of F1() st ( \$1 = s & \$2 = { e where e is Element of (Equations F1()) . s : for A being non-empty MSAlgebra over F1() st P1[A] holds A |= e } ); A6: now__::_thesis:_for_w_being_set_st_w_in_the_carrier_of_F1()_holds_ ex_d_being_set_st_S1[w,d] let w be set ; ::_thesis: ( w in the carrier of F1() implies ex d being set st S1[w,d] ) assume w in the carrier of F1() ; ::_thesis: ex d being set st S1[w,d] then consider s being SortSymbol of F1() such that A7: s = w ; take d = { e where e is Element of (Equations F1()) . s : for A being non-empty MSAlgebra over F1() st P1[A] holds A |= e } ; ::_thesis: S1[w,d] thus S1[w,d] by A7; ::_thesis: verum end; consider E being ManySortedSet of the carrier of F1() such that A8: for i being set st i in the carrier of F1() holds S1[i,E . i] from PBOOLE:sch_3(A6); E is ManySortedSubset of Equations F1() proof let j be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not j in the carrier of F1() or E . j c= (Equations F1()) . j ) assume j in the carrier of F1() ; ::_thesis: E . j c= (Equations F1()) . j then consider s being SortSymbol of F1() such that A9: j = s and A10: E . j = { e where e is Element of (Equations F1()) . s : for A being non-empty MSAlgebra over F1() st P1[A] holds A |= e } by A8; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in E . j or q in (Equations F1()) . j ) assume q in E . j ; ::_thesis: q in (Equations F1()) . j then ex z being Element of (Equations F1()) . s st ( q = z & ( for A being non-empty MSAlgebra over F1() st P1[A] holds A |= z ) ) by A10; hence q in (Equations F1()) . j by A9; ::_thesis: verum end; then reconsider E = E as EqualSet of F1() ; A11: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds P1[B] by A1; defpred S2[ MSAlgebra over F1()] means \$1 |= E; A12: for D being non-empty MSAlgebra over F1() holds ( S2[D] iff for s being SortSymbol of F1() for e being Element of (Equations F1()) . s st ( for M being non-empty MSAlgebra over F1() st P1[M] holds M |= e ) holds D |= e ) proof let D be non-empty MSAlgebra over F1(); ::_thesis: ( S2[D] iff for s being SortSymbol of F1() for e being Element of (Equations F1()) . s st ( for M being non-empty MSAlgebra over F1() st P1[M] holds M |= e ) holds D |= e ) thus ( S2[D] implies for s being SortSymbol of F1() for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra over F1() st P1[B] holds B |= e ) holds D |= e ) ::_thesis: ( ( for s being SortSymbol of F1() for e being Element of (Equations F1()) . s st ( for M being non-empty MSAlgebra over F1() st P1[M] holds M |= e ) holds D |= e ) implies S2[D] ) proof assume A13: S2[D] ; ::_thesis: for s being SortSymbol of F1() for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra over F1() st P1[B] holds B |= e ) holds D |= e let s be SortSymbol of F1(); ::_thesis: for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra over F1() st P1[B] holds B |= e ) holds D |= e let e be Element of (Equations F1()) . s; ::_thesis: ( ( for B being non-empty MSAlgebra over F1() st P1[B] holds B |= e ) implies D |= e ) assume A14: for B being non-empty MSAlgebra over F1() st P1[B] holds B |= e ; ::_thesis: D |= e S1[s,E . s] by A8; then e in E . s by A14; hence D |= e by A13, EQUATION:def_6; ::_thesis: verum end; assume A15: for s being SortSymbol of F1() for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra over F1() st P1[B] holds B |= e ) holds D |= e ; ::_thesis: S2[D] let s be SortSymbol of F1(); :: according to EQUATION:def_6 ::_thesis: for b1 being Element of (Equations F1()) . s holds ( not b1 in E . s or D |= b1 ) let e be Element of (Equations F1()) . s; ::_thesis: ( not e in E . s or D |= e ) assume A16: e in E . s ; ::_thesis: D |= e S1[s,E . s] by A8; then ex f being Element of (Equations F1()) . s st ( e = f & ( for A being non-empty MSAlgebra over F1() st P1[A] holds A |= f ) ) by A16; hence D |= e by A15; ::_thesis: verum end; A17: for A being non-empty MSAlgebra over F1() for B being strict non-empty MSSubAlgebra of A st S2[A] holds S2[B] by EQUATION:32; A18: for I being set for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds ex A being MSAlgebra over F1() st ( A = F . i & S2[A] ) ) holds S2[ product F] by EQUATION:38; A19: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & S2[A] holds S2[B] by EQUATION:34; consider K being strict non-empty MSAlgebra over F1(), F being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of K such that A20: S2[K] and A21: for B being non-empty MSAlgebra over F1() for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of B st S2[B] holds ex H being ManySortedFunction of K,B st ( H is_homomorphism K,B & H ** F = G & ( for W being ManySortedFunction of K,B st W is_homomorphism K,B & W ** F = G holds H = W ) ) from BIRKHOFF:sch_2(A19, A17, A18); A22: for M being non-empty MSAlgebra over F1() for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of M st S2[M] holds ex H being ManySortedFunction of K,M st ( H is_homomorphism K,M & G = H ** F ) proof let M be non-empty MSAlgebra over F1(); ::_thesis: for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of M st S2[M] holds ex H being ManySortedFunction of K,M st ( H is_homomorphism K,M & G = H ** F ) let G be ManySortedFunction of the carrier of F1() --> NAT, the Sorts of M; ::_thesis: ( S2[M] implies ex H being ManySortedFunction of K,M st ( H is_homomorphism K,M & G = H ** F ) ) assume S2[M] ; ::_thesis: ex H being ManySortedFunction of K,M st ( H is_homomorphism K,M & G = H ** F ) then ex H being ManySortedFunction of K,M st ( H is_homomorphism K,M & H ** F = G & ( for W being ManySortedFunction of K,M st W is_homomorphism K,M & W ** F = G holds H = W ) ) by A21; hence ex H being ManySortedFunction of K,M st ( H is_homomorphism K,M & H ** F = G ) ; ::_thesis: verum end; A23: for I being set for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds ex A being MSAlgebra over F1() st ( A = F . i & P1[A] ) ) holds P1[ product F] by A4; take E ; ::_thesis: for A being non-empty MSAlgebra over F1() holds ( P1[A] iff A |= E ) let A be non-empty MSAlgebra over F1(); ::_thesis: ( P1[A] iff A |= E ) hereby ::_thesis: ( A |= E implies P1[A] ) assume A24: P1[A] ; ::_thesis: A |= E thus A |= E ::_thesis: verum proof let s1 be SortSymbol of F1(); :: according to EQUATION:def_6 ::_thesis: for b1 being Element of (Equations F1()) . s1 holds ( not b1 in E . s1 or A |= b1 ) A25: S1[s1,E . s1] by A8; let e be Element of (Equations F1()) . s1; ::_thesis: ( not e in E . s1 or A |= e ) assume e in E . s1 ; ::_thesis: A |= e then consider x being Element of (Equations F1()) . s1 such that A26: e = x and A27: for A being non-empty MSAlgebra over F1() st P1[A] holds A |= x by A25; A28: A |= x by A24, A27; let h be ManySortedFunction of (TermAlg F1()),A; :: according to EQUATION:def_5 ::_thesis: ( not h is_homomorphism TermAlg F1(),A or (h . s1) . (e `1) = (h . s1) . (e `2) ) assume h is_homomorphism TermAlg F1(),A ; ::_thesis: (h . s1) . (e `1) = (h . s1) . (e `2) hence (h . s1) . (e `1) = (h . s1) . (e `2) by A26, A28, EQUATION:def_5; ::_thesis: verum end; end; assume A29: A |= E ; ::_thesis: P1[A] A30: for A being non-empty MSAlgebra over F1() for R being MSCongruence of A st P1[A] holds P1[ QuotMSAlg (A,R)] by A3; A31: S2[K] by A20; A32: P1[K] from BIRKHOFF:sch_11(A12, A21, A31, A11, A5, A23); A33: for B being strict non-empty finitely-generated MSSubAlgebra of A holds P1[B] proof let B be strict non-empty finitely-generated MSSubAlgebra of A; ::_thesis: P1[B] A34: S2[B] by A29, EQUATION:32; thus P1[B] from BIRKHOFF:sch_7(A34, A32, A22, A11, A30); ::_thesis: verum end; thus P1[A] from BIRKHOFF:sch_9(A33, A11, A5, A30, A23); ::_thesis: verum end;