set EMF = the MSAlgebra-Family of {} ,F₁();
set CC = { C where C is Element of (CongrLatt F₂()) : ex R being MSCongruence of F₂() st
( R = C & P₁[ QuotMSAlg (F₂(),R)] ) } ;
set SF = the Sorts of F₂();
set I = the carrier of F₁();
consider Xi being ManySortedSet of the carrier of F₁() such that
A4: {Xi} = the carrier of F₁() --> {{}} by MSUALG_9:5;

let i be object ; :: thesis:
assume i in the carrier of F₁() ; :: thesis:
then reconsider s = i as SortSymbol of F₁() ;
thus the Sorts of (product the MSAlgebra-Family of {} ,F₁()) . i = product (Carrier ( the MSAlgebra-Family of {} ,F₁(),s)) by PRALG_2:def 10
.= {{}} by CARD_3:10, PRALG_2:def 9
.= ( the carrier of F₁() --> {{}}) . s
.= {Xi} . i by A4 ; :: thesis:

end;

then A5: the Sorts of (product the MSAlgebra-Family of {} ,F₁()) = {Xi} ;
reconsider R = [| the Sorts of F₂(), the Sorts of F₂()|] as MSCongruence of F₂() by MSUALG_5:18;
[| the Sorts of F₂(), the Sorts of F₂()|] is MSCongruence of F₂() by MSUALG_5:18;
then A6: [| the Sorts of F₂(), the Sorts of F₂()|] is Element of (CongrLatt F₂()) by MSUALG_5:def 6;
the Sorts of (QuotMSAlg (F₂(),R)) = { the Sorts of F₂()} by MSUALG_9:29;
then A7: QuotMSAlg (F₂(),R), Trivial_Algebra F₁() are_isomorphic by MSUALG_9:26;
for i being set st i in {} holds
ex A being MSAlgebra over F₁() st
( A = the MSAlgebra-Family of {} ,F₁() . i & P₁[A] ) ;
then P₁[ product the MSAlgebra-Family of {} ,F₁()] by A3;
then P₁[ Trivial_Algebra F₁()] by A1, A5, MSUALG_9:26;
then P₁[ QuotMSAlg (F₂(),R)] by A1, A7, MSUALG_3:17;
then A8: [| the Sorts of F₂(), the Sorts of F₂()|] in { C where C is Element of (CongrLatt F₂()) : ex R being MSCongruence of F₂() st
( R = C & P₁[ QuotMSAlg (F₂(),R)] ) } by A6;
defpred S₁[ object , object ] means ex R being MSCongruence of F₂() st
( R = $1 & $2 = QuotMSAlg (F₂(),R) );
defpred S₂[ set ] means ex R being MSCongruence of F₂() st
( R = $1 & P₁[ QuotMSAlg (F₂(),R)] );

A9: now :: thesis:

let q be object ; :: thesis:
assume q in { C where C is Element of (CongrLatt F₂()) : ex R being MSCongruence of F₂() st
( R = C & P₁[ QuotMSAlg (F₂(),R)] ) } ; :: thesis:
then ex C being Element of (CongrLatt F₂()) st
( q = C & ex R being MSCongruence of F₂() st
( R = C & P₁[ QuotMSAlg (F₂(),R)] ) ) ;
hence q is MSCongruence of F₂() ; :: thesis:

end;

A10: { C where C is Element of (CongrLatt F₂()) : ex R being MSCongruence of F₂() st
( R = C & P₁[ QuotMSAlg (F₂(),R)] ) } c= the carrier of (EqRelLatt the Sorts of F₂())

proof

let q be object ; :: according to TARSKI:def 3 :: thesis:
assume q in { C where C is Element of (CongrLatt F₂()) : ex R being MSCongruence of F₂() st
( R = C & P₁[ QuotMSAlg (F₂(),R)] ) } ; :: thesis:
then q is Equivalence_Relation of the Sorts of F₂() by A9;
hence q in the carrier of (EqRelLatt the Sorts of F₂()) by MSUALG_5:def 5; :: thesis:

end;

then reconsider CC = { C where C is Element of (CongrLatt F₂()) : ex R being MSCongruence of F₂() st
( R = C & P₁[ QuotMSAlg (F₂(),R)] ) } as non empty SubsetFamily of [| the Sorts of F₂(), the Sorts of F₂()|] by A8, MSUALG_7:5;
set R0 = meet |:CC:|;
A11: meet |:CC:| is MSEquivalence_Relation-like ManySortedRelation of the Sorts of F₂() by A10, MSUALG_7:8;
reconsider R0 = meet |:CC:| as ManySortedRelation of F₂() by A10, MSUALG_7:8;
R0 is MSEquivalence-like by A11;
then reconsider R0 = R0 as MSEquivalence-like ManySortedRelation of F₂() ;
{ C where C is Element of (CongrLatt F₂()) : S₂[C] } is Subset of (CongrLatt F₂()) from DOMAIN_1:sch 7();
then reconsider R0 = R0 as MSCongruence of F₂() by MSUALG_9:28;
take A = QuotMSAlg (F₂(),R0); :: thesis:
reconsider F = MSNat_Hom (F₂(),R0) as ManySortedFunction of F₂(),A ;
take F ; :: thesis:

A12: now :: thesis:

let c be object ; :: thesis:
assume c in CC ; :: thesis:
then reconsider cc = c as MSCongruence of F₂() by A9;
reconsider w = QuotMSAlg (F₂(),cc) as object ;
take w = w; :: thesis:
thus S₁[c,w] ; :: thesis:

end;

consider FF being ManySortedSet of CC such that
A13: for c being object st c in CC holds
S₁[c,FF . c] from PBOOLE:sch 3(A12);
FF is MSAlgebra-Family of CC,F₁()

proof

let c be object ; :: according to PRALG_2:def 5 :: thesis:
assume c in CC ; :: thesis:
then ex R being MSCongruence of F₂() st
( R = c & FF . c = QuotMSAlg (F₂(),R) ) by A13;
hence FF . c is MSAlgebra over F₁() ; :: thesis:

end;

then reconsider FF = FF as MSAlgebra-Family of CC,F₁() ;
defpred S₃[ Element of CC, object ] means ex F1 being ManySortedFunction of F₂(),(FF . $1) st
( F1 = $2 & F1 is_homomorphism F₂(),FF . $1 & ex R being MSCongruence of F₂() st
( $1 = R & F1 = MSNat_Hom (F₂(),R) ) );
A14: for c being Element of CC ex j being object st S₃[c,j]

proof

let c be Element of CC; :: thesis:
consider R being MSCongruence of F₂() such that
A15: R = c and
A16: FF . c = QuotMSAlg (F₂(),R) by A13;
set j = MSNat_Hom (F₂(),R);
reconsider F1 = MSNat_Hom (F₂(),R) as ManySortedFunction of F₂(),(FF . c) by A16;
take MSNat_Hom (F₂(),R) ; :: thesis:
take F1 ; :: thesis:
thus F1 = MSNat_Hom (F₂(),R) ; :: thesis:
MSNat_Hom (F₂(),R) is_epimorphism F₂(), QuotMSAlg (F₂(),R) by MSUALG_4:3;
hence F1 is_homomorphism F₂(),FF . c by A16, MSUALG_3:def 8; :: thesis:
take R ; :: thesis:
thus ( c = R & F1 = MSNat_Hom (F₂(),R) ) by A15; :: thesis:

end;

consider FofI1 being ManySortedSet of CC such that
A17: for c being Element of CC holds S₃[c,FofI1 . c] from PBOOLE:sch 6(A14);
A18: for c being Element of CC ex F1 being ManySortedFunction of F₂(),(FF . c) st
( F1 = FofI1 . c & F1 is_homomorphism F₂(),FF . c )

proof

let c be Element of CC; :: thesis:
consider F1 being ManySortedFunction of F₂(),(FF . c) such that
A19: F1 = FofI1 . c and
A20: F1 is_homomorphism F₂(),FF . c and
ex R being MSCongruence of F₂() st
( c = R & F1 = MSNat_Hom (F₂(),R) ) by A17;
take F1 ; :: thesis:
thus ( F1 = FofI1 . c & F1 is_homomorphism F₂(),FF . c ) by A19, A20; :: thesis:

end;

FofI1 is Function-yielding

proof

let c be object ; :: according to FUNCOP_1:def 6 :: thesis:
assume c in dom FofI1 ; :: thesis:
then reconsider cc = c as Element of CC ;
ex F1 being ManySortedFunction of F₂(),(FF . cc) st
( F1 = FofI1 . cc & F1 is_homomorphism F₂(),FF . cc ) by A18;
hence FofI1 . c is set ; :: thesis:

end;

then reconsider FofI1 = FofI1 as ManySortedFunction of CC ;
consider H being ManySortedFunction of F₂(),(product FF) such that
A21: H is_homomorphism F₂(), product FF and
A22: for c being Element of CC holds (proj (FF,c)) ** H = FofI1 . c by A18, PRALG_3:29;

now :: thesis:

let i be object ; :: thesis:
assume i in the carrier of F₁() ; :: thesis:
then reconsider s = i as SortSymbol of F₁() ;
consider Q being Subset-Family of ([| the Sorts of F₂(), the Sorts of F₂()|] . s) such that
A23: Q = |:CC:| . s and
A24: (meet |:CC:|) . s = Intersect Q by MSSUBFAM:def 1;
A25: |:CC:| . s = { (t . s) where t is Element of Bool [| the Sorts of F₂(), the Sorts of F₂()|] : t in CC } by CLOSURE2:14;
(MSCng H) . s = R0 . s

proof

let a, b be object ; :: according to RELAT_1:def 2 :: thesis:

hereby :: thesis:

assume A26: [a,b] in (MSCng H) . s ; :: thesis:
then A27: a in the Sorts of F₂() . s by ZFMISC_1:87;
A28: b in the Sorts of F₂() . s by A26, ZFMISC_1:87;
A29: [a,b] in MSCng (H,s) by A21, A26, MSUALG_4:def 18;
A30: for Y being set st Y in Q holds
[a,b] in Y

proof

let Y be set ; :: thesis:
assume Y in Q ; :: thesis:
then consider t being Element of Bool [| the Sorts of F₂(), the Sorts of F₂()|] such that
A31: Y = t . s and
A32: t in CC by A23, A25;
reconsider t1 = t as Element of CC by A32;
consider F1 being ManySortedFunction of F₂(),(FF . t1) such that
A33: F1 = FofI1 . t1 and
F1 is_homomorphism F₂(),FF . t1 and
A34: ex R being MSCongruence of F₂() st
( t1 = R & F1 = MSNat_Hom (F₂(),R) ) by A17;
(F1 . s) . a = (((proj (FF,t1)) ** H) . s) . a by A22, A33
.= (((proj (FF,t1)) . s) * (H . s)) . a by MSUALG_3:2
.= ((proj (FF,t1)) . s) . ((H . s) . a) by A27, FUNCT_2:15
.= ((proj (FF,t1)) . s) . ((H . s) . b) by A27, A28, A29, MSUALG_4:def 17
.= (((proj (FF,t1)) . s) * (H . s)) . b by A28, FUNCT_2:15
.= (((proj (FF,t1)) ** H) . s) . b by MSUALG_3:2
.= (F1 . s) . b by A22, A33 ;
hence [a,b] in Y by A27, A28, A31, A34, MSUALG_9:33; :: thesis:

end;

[a,b] in [:( the Sorts of F₂() . s),( the Sorts of F₂() . s):] by A26;
then [a,b] in [| the Sorts of F₂(), the Sorts of F₂()|] . s by PBOOLE:def 16;
hence [a,b] in R0 . s by A24, A30, SETFAM_1:43; :: thesis:

end;

assume A35: [a,b] in R0 . s ; :: thesis:
then A36: a in the Sorts of F₂() . s by ZFMISC_1:87;
A37: b in the Sorts of F₂() . s by A35, ZFMISC_1:87;
A38: 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:
reconsider t1 = c as MSCongruence of F₂() by A9;
consider F1 being ManySortedFunction of F₂(),(FF . c) such that
A39: F1 = FofI1 . c and
F1 is_homomorphism F₂(),FF . c and
A40: ex R being MSCongruence of F₂() st
( c = R & F1 = MSNat_Hom (F₂(),R) ) by A17;
t1 is Element of Bool [| the Sorts of F₂(), the Sorts of F₂()|] by CLOSURE2:def 1;
then t1 . s in |:CC:| . s by A25;
then A41: [a,b] in t1 . s by A23, A24, A35, SETFAM_1:43;
thus (proj ((Carrier (FF,s)),c)) . ((H . s) . a) = ((proj (FF,c)) . s) . ((H . s) . a) by PRALG_3:def 2
.= (((proj (FF,c)) . s) * (H . s)) . a by A36, FUNCT_2:15
.= (((proj (FF,c)) ** H) . s) . a by MSUALG_3:2
.= (F1 . s) . a by A22, A39
.= (F1 . s) . b by A36, A37, A41, A40, MSUALG_9:33
.= (((proj (FF,c)) ** H) . s) . b by A22, A39
.= (((proj (FF,c)) . s) * (H . s)) . b by MSUALG_3:2
.= ((proj (FF,c)) . s) . ((H . s) . b) by A37, FUNCT_2:15
.= (proj ((Carrier (FF,s)),c)) . ((H . s) . b) by PRALG_3:def 2 ; :: thesis:

end;

(H . s) . b in the Sorts of (product FF) . s by A37, FUNCT_2:5;
then A42: (H . s) . b in product (Carrier (FF,s)) by PRALG_2:def 10;
(H . s) . a in the Sorts of (product FF) . s by A36, FUNCT_2:5;
then (H . s) . a in product (Carrier (FF,s)) by PRALG_2:def 10;
then (H . s) . a = (H . s) . b by A42, A38, MSUALG_9:14;
then [a,b] in MSCng (H,s) by A36, A37, MSUALG_4:def 17;
hence [a,b] in (MSCng H) . s by A21, MSUALG_4:def 18; :: thesis:

end;

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

end;

then A43: MSCng H = R0 ;
QuotMSAlg (F₂(),(MSCng H)), Image (MSHomQuot H) are_isomorphic by A21, MSUALG_4:4, MSUALG_9:16;
then consider XX being strict non-empty MSSubAlgebra of product FF such that
A44: A,XX are_isomorphic by A43;
for cc being set st cc in CC holds
ex A being MSAlgebra over F₁() st
( A = FF . cc & P₁[A] )

proof

let cc be set ; :: thesis:
assume A45: cc in CC ; :: thesis:
then reconsider c = cc as Element of CC ;
take FF . c ; :: thesis:
A46: ex C being Element of (CongrLatt F₂()) st
( cc = C & ex R being MSCongruence of F₂() st
( R = C & P₁[ QuotMSAlg (F₂(),R)] ) ) by A45;
ex R being MSCongruence of F₂() st
( R = cc & FF . cc = QuotMSAlg (F₂(),R) ) by A13, A45;
hence ( FF . c = FF . cc & P₁[FF . c] ) by A46; :: thesis:

end;

then P₁[XX] by A2, A3;
hence P₁[A] by A1, A44, MSUALG_3:17; :: thesis:
thus F is_epimorphism F₂(),A by MSUALG_4:3; :: thesis:
then A47: F is "onto" by MSUALG_3:def 8;
let B be non-empty MSAlgebra over F₁(); :: thesis:
let G be ManySortedFunction of F₂(),B; :: thesis:
assume that
A48: G is_homomorphism F₂(),B and
A49: P₁[B] ; :: thesis:
reconsider C = Image (MSHomQuot G) as strict non-empty MSSubAlgebra of B ;
A50: QuotMSAlg (F₂(),(MSCng G)),C are_isomorphic by A48, MSUALG_4:4, MSUALG_9:16;
A51: MSCng G is Element of (CongrLatt F₂()) by MSUALG_5:def 6;
P₁[C] by A2, A49;
then P₁[ QuotMSAlg (F₂(),(MSCng G))] by A1, A50, MSUALG_3:17;
then MSCng G in CC by A51;
then R0 c= MSCng G by CLOSURE2:21, MSSUBFAM:43;
then consider H being ManySortedFunction of A,B such that
A52: H is_homomorphism A,B and
A53: G = H ** F by A48, MSUALG_9:36;
take H ; :: thesis:
thus H is_homomorphism A,B by A52; :: thesis:
thus G = H ** F by A53; :: thesis:
let K be ManySortedFunction of A,B; :: thesis:
assume K ** F = G ; :: thesis:
hence H = K by A53, A47, EXTENS_1:12; :: thesis: