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