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 object st i in the carrier of F1() holds
the Sorts of (product the MSAlgebra-Family of {} ,F1()) . i = {Xi} . i
let i be object ; :: 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
.= ( the carrier of F1() --> ) . s
.= {Xi} . i by A4 ; :: thesis: verum
end;
then A5: the Sorts of (product the MSAlgebra-Family of {} ,F1()) = {Xi} ;
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 ;
then P1[ QuotMSAlg (F2(),R)] by ;
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[ object , object ] 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 object 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 object ; :: 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 object ; :: 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 ;
set R0 = meet |:CC:|;
A11: meet |:CC:| is MSEquivalence_Relation-like ManySortedRelation of the Sorts of F2() by ;
reconsider R0 = meet |:CC:| as ManySortedRelation of F2() by ;
R0 is MSEquivalence-like by A11;
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 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 ) ) ) )

A12: now :: thesis: for c being object st c in CC holds
ex w being object st S1[c,w]
let c be object ; :: thesis: ( c in CC implies ex w being object st S1[c,w] )
assume c in CC ; :: thesis: ex w being object st S1[c,w]
then reconsider cc = c as MSCongruence of F2() by A9;
reconsider w = QuotMSAlg (F2(),cc) as object ;
take w = w; :: thesis: S1[c,w]
thus S1[c,w] ; :: thesis: verum
end;
consider FF being ManySortedSet of CC such that
A13: for c being object st c in CC holds
S1[c,FF . c] from FF is MSAlgebra-Family of CC,F1()
proof
let c be object ; :: 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 A13;
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, object ] 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) ) );
A14: for c being Element of CC ex j being object st S3[c,j]
proof
let c be Element of CC; :: thesis: ex j being object st S3[c,j]
consider R being MSCongruence of F2() such that
A15: R = c and
A16: FF . c = QuotMSAlg (F2(),R) by A13;
set j = MSNat_Hom (F2(),R);
reconsider F1 = MSNat_Hom (F2(),R) as ManySortedFunction of F2(),(FF . c) by A16;
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 ; :: 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 A15; :: thesis: verum
end;
consider FofI1 being ManySortedSet of CC such that
A17: for c being Element of CC holds S3[c,FofI1 . c] from A18: 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
A19: F1 = FofI1 . c and
A20: F1 is_homomorphism F2(),FF . c and
ex R being MSCongruence of F2() st
( c = R & F1 = MSNat_Hom (F2(),R) ) by A17;
take F1 ; :: thesis: ( F1 = FofI1 . c & F1 is_homomorphism F2(),FF . c )
thus ( F1 = FofI1 . c & F1 is_homomorphism F2(),FF . c ) by ; :: thesis: verum
end;
FofI1 is Function-yielding
proof
let c be object ; :: 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 A18;
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
A21: H is_homomorphism F2(), product FF and
A22: for c being Element of CC holds (proj (FF,c)) ** H = FofI1 . c by ;
now :: thesis: for i being object st i in the carrier of F1() holds
() . i = R0 . i
let i be object ; :: thesis: ( i in the carrier of F1() implies () . i = R0 . i )
assume i in the carrier of F1() ; :: thesis: () . 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
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 F2(), the Sorts of F2()|] : t in CC } by CLOSURE2:14;
(MSCng H) . s = R0 . s
proof
let a, b be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in () . s or [a,b] in R0 . s ) & ( not [a,b] in R0 . s or [a,b] in () . s ) )
hereby :: thesis: ( not [a,b] in R0 . s or [a,b] in () . s )
assume A26: [a,b] in () . s ; :: thesis: [a,b] in R0 . s
then A27: a in the Sorts of F2() . s by ZFMISC_1:87;
A28: b in the Sorts of F2() . s by ;
A29: [a,b] in MSCng (H,s) by ;
A30: 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
A31: Y = t . s and
A32: t in CC by ;
reconsider t1 = t as Element of CC by A32;
consider F1 being ManySortedFunction of F2(),(FF . t1) such that
A33: F1 = FofI1 . t1 and
F1 is_homomorphism F2(),FF . t1 and
A34: ex R being MSCongruence of F2() st
( t1 = R & F1 = MSNat_Hom (F2(),R) ) by A17;
(F1 . s) . a = (((proj (FF,t1)) ** H) . s) . a by
.= (((proj (FF,t1)) . s) * (H . s)) . a by MSUALG_3:2
.= ((proj (FF,t1)) . s) . ((H . s) . a) by
.= ((proj (FF,t1)) . s) . ((H . s) . b) by
.= (((proj (FF,t1)) . s) * (H . s)) . b by
.= (((proj (FF,t1)) ** H) . s) . b by MSUALG_3:2
.= (F1 . s) . b by ;
hence [a,b] in Y by ; :: thesis: verum
end;
[a,b] in [:( the Sorts of F2() . s),( the Sorts of F2() . s):] by A26;
then [a,b] in [| the Sorts of F2(), the Sorts of F2()|] . s by PBOOLE:def 16;
hence [a,b] in R0 . s by ; :: thesis: verum
end;
assume A35: [a,b] in R0 . s ; :: thesis: [a,b] in () . s
then A36: a in the Sorts of F2() . s by ZFMISC_1:87;
A37: b in the Sorts of F2() . s by ;
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: (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
A39: F1 = FofI1 . c and
F1 is_homomorphism F2(),FF . c and
A40: ex R being MSCongruence of F2() st
( c = R & F1 = MSNat_Hom (F2(),R) ) by A17;
t1 is Element of Bool [| the Sorts of F2(), the Sorts of F2()|] by CLOSURE2:def 1;
then t1 . s in |:CC:| . s by A25;
then A41: [a,b] in t1 . s by ;
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
.= (((proj (FF,c)) ** H) . s) . a by MSUALG_3:2
.= (F1 . s) . a by
.= (F1 . s) . b by
.= (((proj (FF,c)) ** H) . s) . b by
.= (((proj (FF,c)) . s) * (H . s)) . b by MSUALG_3:2
.= ((proj (FF,c)) . s) . ((H . s) . b) by
.= (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 ;
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 ;
then (H . s) . a in product (Carrier (FF,s)) by PRALG_2:def 10;
then (H . s) . a = (H . s) . b by ;
then [a,b] in MSCng (H,s) by ;
hence [a,b] in () . s by ; :: thesis: verum
end;
hence (MSCng H) . i = R0 . i ; :: thesis: verum
end;
then A43: MSCng H = R0 ;
QuotMSAlg (F2(),()), Image () are_isomorphic by ;
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 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 A45: 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] )
A46: ex C being Element of (CongrLatt F2()) st
( cc = C & ex R being MSCongruence of F2() st
( R = C & P1[ QuotMSAlg (F2(),R)] ) ) by A45;
ex R being MSCongruence of F2() st
( R = cc & FF . cc = QuotMSAlg (F2(),R) ) by ;
hence ( FF . c = FF . cc & P1[FF . c] ) by A46; :: thesis: verum
end;
then P1[XX] by A2, A3;
hence P1[A] by A1, A44, 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 A47: 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
A48: G is_homomorphism F2(),B and
A49: 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 () as strict non-empty MSSubAlgebra of B ;
A50: QuotMSAlg (F2(),()),C are_isomorphic by ;
A51: MSCng G is Element of (CongrLatt F2()) by MSUALG_5:def 6;
P1[C] by A2, A49;
then P1[ QuotMSAlg (F2(),())] by ;
then MSCng G in CC by A51;
then R0 c= MSCng G by ;
then consider H being ManySortedFunction of A,B such that
A52: H is_homomorphism A,B and
A53: G = H ** F by ;
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 A52; :: thesis: ( H ** F = G & ( for K being ManySortedFunction of A,B st K ** F = G holds
H = K ) )

thus G = H ** F by A53; :: 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 ; :: thesis: verum