consider EMF being 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:6;

let i be set ; :: thesis:
assume i in the carrier of F₁() ; :: thesis:
then reconsider s = i as SortSymbol of F₁() ;
thus the Sorts of (product EMF) . i = product (Carrier (EMF,s)) by PRALG_2:def 17
.= {{}} by CARD_3:19, PRALG_2:def 16
.= ( the carrier of F₁() --> {{}}) . s by FUNCOP_1:13
.= {Xi} . i by A4 ; :: thesis:

end;

then A5: the Sorts of (product EMF) = {Xi} by PBOOLE:3;
reconsider R = [| the Sorts of F₂(), the Sorts of F₂()|] as MSCongruence of F₂() by MSUALG_5:20;
[| the Sorts of F₂(), the Sorts of F₂()|] is MSCongruence of F₂() by MSUALG_5:20;
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:30;
then A7: QuotMSAlg (F₂(),R), Trivial_Algebra F₁() are_isomorphic by MSUALG_9:27;
for i being set st i in {} holds
ex A being MSAlgebra of F₁() st
( A = EMF . i & P₁[A] ) ;
then P₁[ product EMF] by A3;
then P₁[ Trivial_Algebra F₁()] by A1, A5, MSUALG_9:27;
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₁[ set , set ] 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

let q be set ; :: 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 set ; :: 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:6;
set R0 = meet |:CC:|;
A11: meet |:CC:| is MSEquivalence_Relation-like ManySortedRelation of the Sorts of F₂() by A10, MSUALG_7:9;
reconsider R0 = meet |:CC:| as ManySortedRelation of F₂() by A10, MSUALG_7:9;
R0 is MSEquivalence-like

proof

let i be set ; :: according to MSUALG_4:def 3,MSUALG_4:def 5 :: thesis:
let R be Relation of ( the Sorts of F₂() . i); :: thesis:
assume that
A12: i in the carrier of F₁() and
A13: R0 . i = R ; :: thesis:
thus R is Element of bool [:( the Sorts of F₂() . i),( the Sorts of F₂() . i):] by A11, A12, A13, MSUALG_4:def 3; :: thesis:

end;

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:29;
take A = QuotMSAlg (F₂(),R0); :: thesis:
reconsider F = MSNat_Hom (F₂(),R0) as ManySortedFunction of F₂(),A ;
take F ; :: thesis:

A14: now

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

end;

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

proof

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

end;

then reconsider FF = FF as MSAlgebra-Family of CC,F₁() ;
defpred S₃[ Element of CC, set ] 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) ) );
A17: for c being Element of CC ex j being set st S₃[c,j]

proof

let c be Element of CC; :: thesis:
consider R being MSCongruence of F₂() such that
A18: R = c and
A19: FF . c = QuotMSAlg (F₂(),R) by A16;
set j = MSNat_Hom (F₂(),R);
reconsider F1 = MSNat_Hom (F₂(),R) as ManySortedFunction of F₂(),(FF . c) by A19;
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 A19, MSUALG_3:def 10; :: thesis:
take R ; :: thesis:
thus ( c = R & F1 = MSNat_Hom (F₂(),R) ) by A18; :: thesis:

end;

consider FofI1 being ManySortedSet of CC such that
A20: for c being Element of CC holds S₃[c,FofI1 . c] from PBOOLE:sch 6(A17);
A21: 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
A22: F1 = FofI1 . c and
A23: F1 is_homomorphism F₂(),FF . c and
ex R being MSCongruence of F₂() st
( c = R & F1 = MSNat_Hom (F₂(),R) ) by A20;
take F1 ; :: thesis:
thus ( F1 = FofI1 . c & F1 is_homomorphism F₂(),FF . c ) by A22, A23; :: thesis:

end;

FofI1 is Function-yielding

proof

let c be set ; :: according to FUNCOP_1:def 6 :: thesis:
assume c in dom FofI1 ; :: thesis:
then reconsider cc = c as Element of CC by PARTFUN1:def 4;
ex F1 being ManySortedFunction of F₂(),(FF . cc) st
( F1 = FofI1 . cc & F1 is_homomorphism F₂(),FF . cc ) by A21;
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
A24: H is_homomorphism F₂(), product FF and
A25: for c being Element of CC holds (proj (FF,c)) ** H = FofI1 . c by A21, PRALG_3:30;

now

let i be set ; :: 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
A26: Q = |:CC:| . s and
A27: (meet |:CC:|) . s = Intersect Q by MSSUBFAM:def 2;
A28: |:CC:| . s = { (t . s) where t is Element of Bool [| the Sorts of F₂(), the Sorts of F₂()|] : t in CC } by CLOSURE2:15;
(MSCng H) . s = R0 . s

proof

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

hereby :: thesis:

assume A29: [a,b] in (MSCng H) . s ; :: thesis:
then A30: a in the Sorts of F₂() . s by ZFMISC_1:106;
A31: b in the Sorts of F₂() . s by A29, ZFMISC_1:106;
A32: [a,b] in MSCng (H,s) by A24, A29, MSUALG_4:def 20;
A33: 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
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 F₂(),(FF . t1) such that
A36: F1 = FofI1 . t1 and
F1 is_homomorphism F₂(),FF . t1 and
A37: ex R being MSCongruence of F₂() st
( t1 = R & F1 = MSNat_Hom (F₂(),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:21
.= ((proj (FF,t1)) . s) . ((H . s) . b) by A30, A31, A32, MSUALG_4:def 19
.= (((proj (FF,t1)) . s) * (H . s)) . b by A31, FUNCT_2:21
.= (((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:34; :: thesis:

end;

[a,b] in [:( the Sorts of F₂() . s),( the Sorts of F₂() . s):] by A29;
then [a,b] in [| the Sorts of F₂(), the Sorts of F₂()|] . s by PBOOLE:def 21;
hence [a,b] in R0 . s by A27, A33, SETFAM_1:58; :: thesis:

end;

assume A38: [a,b] in R0 . s ; :: thesis:
then A39: a in the Sorts of F₂() . s by ZFMISC_1:106;
A40: b in the Sorts of F₂() . s by A38, ZFMISC_1:106;
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:
reconsider t1 = c as MSCongruence of F₂() by A9;
consider F1 being ManySortedFunction of F₂(),(FF . c) such that
A42: F1 = FofI1 . c and
F1 is_homomorphism F₂(),FF . c and
A43: ex R being MSCongruence of F₂() st
( c = R & F1 = MSNat_Hom (F₂(),R) ) by A20;
t1 is Element of Bool [| the Sorts of F₂(), the Sorts of F₂()|] 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:58;
thus (proj ((Carrier (FF,s)),c)) . ((H . s) . a) = ((proj (FF,c)) . s) . ((H . s) . a) by PRALG_3:def 3
.= (((proj (FF,c)) . s) * (H . s)) . a by A39, FUNCT_2:21
.= (((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:34
.= (((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:21
.= (proj ((Carrier (FF,s)),c)) . ((H . s) . b) by PRALG_3:def 3 ; :: thesis:

end;

(H . s) . b in the Sorts of (product FF) . s by A40, FUNCT_2:7;
then A45: (H . s) . b in product (Carrier (FF,s)) by PRALG_2:def 17;
(H . s) . a in the Sorts of (product FF) . s by A39, FUNCT_2:7;
then (H . s) . a in product (Carrier (FF,s)) by PRALG_2:def 17;
then (H . s) . a = (H . s) . b by A45, A41, MSUALG_9:15;
then [a,b] in MSCng (H,s) by A39, A40, MSUALG_4:def 19;
hence [a,b] in (MSCng H) . s by A24, MSUALG_4:def 20; :: thesis:

end;

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

end;

then A46: MSCng H = R0 by PBOOLE:3;
QuotMSAlg (F₂(),(MSCng H)), Image (MSHomQuot H) are_isomorphic by A24, MSUALG_4:4, MSUALG_9:17;
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 of F₁() st
( A = FF . cc & P₁[A] )

proof

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

end;

then P₁[XX] by A2, A3;
hence P₁[A] by A1, A47, MSUALG_3:17; :: thesis:
thus F is_epimorphism F₂(),A by MSUALG_4:3; :: thesis:
then A50: F is "onto" by MSUALG_3:def 10;
let B be non-empty MSAlgebra of F₁(); :: thesis:
let G be ManySortedFunction of F₂(),B; :: thesis:
assume that
A51: G is_homomorphism F₂(),B and
A52: P₁[B] ; :: thesis:
reconsider C = Image (MSHomQuot G) as strict non-empty MSSubAlgebra of B ;
A53: QuotMSAlg (F₂(),(MSCng G)),C are_isomorphic by A51, MSUALG_4:4, MSUALG_9:17;
A54: MSCng G is Element of (CongrLatt F₂()) by MSUALG_5:def 6;
P₁[C] by A2, A52;
then P₁[ QuotMSAlg (F₂(),(MSCng G))] by A1, A53, MSUALG_3:17;
then MSCng G in CC by A54;
then R0 c= MSCng G by CLOSURE2:22, 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:37;
take H ; :: thesis:
thus H is_homomorphism A,B by A55; :: thesis:
thus G = H ** F by A56; :: thesis:
let K be ManySortedFunction of A,B; :: thesis:
assume K ** F = G ; :: thesis:
hence H = K by A56, A50, EXTENS_1:16; :: thesis: