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
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 of 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
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 of 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 of 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
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 of F1() )
assume c in CC ; :: thesis: FF . c is MSAlgebra of F1()
then ex R being MSCongruence of F2() st
( R = c & FF . c = QuotMSAlg (F2(),R) ) by A16;
hence FF . c is MSAlgebra of 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 proj1 FofI1 or FofI1 . c is set )
assume c in dom FofI1 ; :: thesis: FofI1 . c is set
then reconsider cc = c as Element of CC by PARTFUN1:def 2;
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
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 of F1() st
( A = FF . cc & P1[A] )
proof
let cc be set ; :: thesis: ( cc in CC implies ex A being MSAlgebra of F1() st
( A = FF . cc & P1[A] ) )
assume A48: cc in CC ; :: thesis: ex A being MSAlgebra of 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 of 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 of 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 of 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