set SF = the Sorts of F2();
set I = the carrier 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] ) } ;
defpred S1[ set ] means ex R being MSCongruence of F2() st
( R = $1 & P1[ QuotMSAlg F2(),R] );
A4:
{ C where C is Element of (CongrLatt F2()) : S1[C] } is Subset of (CongrLatt F2())
from DOMAIN_1:sch 7();
consider EM being empty set , EMF being MSAlgebra-Family of EM,F1();
for i being set st i in EM holds
ex A being MSAlgebra of F1() st
( A = EMF . i & P1[A] )
;
then A7:
P1[ product EMF]
by A3;
consider Xi being ManySortedSet of the carrier of F1() such that
A8:
{Xi} = the carrier of F1() --> {{} }
by MSUALG_9:6;
then
the Sorts of (product EMF) = {Xi}
by PBOOLE:3;
then A9:
P1[ Trivial_Algebra F1()]
by A1, A7, MSUALG_9:27;
[|the Sorts of F2(),the Sorts of F2()|] is MSCongruence of F2()
by MSUALG_5:20;
then A10:
[|the Sorts of F2(),the Sorts of F2()|] is Element of (CongrLatt F2())
by MSUALG_5:def 6;
reconsider R = [|the Sorts of F2(),the Sorts of F2()|] as MSCongruence of F2() by MSUALG_5:20;
the Sorts of (QuotMSAlg F2(),R) = {the Sorts of F2()}
by MSUALG_9:30;
then consider X being V8 ManySortedSet of the carrier of F1() such that
A11:
the Sorts of (QuotMSAlg F2(),R) = {X}
;
QuotMSAlg F2(),R, Trivial_Algebra F1() are_isomorphic
by A11, MSUALG_9:27;
then
P1[ QuotMSAlg F2(),R]
by A1, A9, MSUALG_3:17;
then A12:
[|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 A10;
A13:
{ 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())
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 A12, MSUALG_7:6;
set R0 = meet |:CC:|;
A14:
meet |:CC:| is MSEquivalence_Relation-like ManySortedRelation of the Sorts of F2()
by A13, MSUALG_7:9;
reconsider R0 = meet |:CC:| as ManySortedRelation of F2() by A13, MSUALG_7:9;
R0 is MSEquivalence-like
then reconsider R0 = R0 as MSEquivalence-like ManySortedRelation of F2() ;
reconsider R0 = R0 as MSCongruence of F2() by A4, MSUALG_9:29;
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 ) ) ) )
defpred S2[ set , set ] means ex R being MSCongruence of F2() st
( R = $1 & $2 = QuotMSAlg F2(),R );
consider FF being ManySortedSet of CC such that
A17:
for c being set st c in CC holds
S2[c,FF . c]
from PBOOLE:sch 3(A15);
FF is MSAlgebra-Family of CC,F1()
then reconsider FF = FF as MSAlgebra-Family of CC,F1() ;
for cc being set st cc in CC holds
ex A being MSAlgebra of F1() st
( A = FF . cc & P1[A] )
then A22:
P1[ product FF]
by A3;
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 ) ) ) )
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 ) );
A23:
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 A24:
(
R = c &
FF . c = QuotMSAlg F2(),
R )
by A17;
set j =
MSNat_Hom F2(),
R;
take
MSNat_Hom F2(),
R
;
:: thesis: S3[c, MSNat_Hom F2(),R]
reconsider F1 =
MSNat_Hom F2(),
R as
ManySortedFunction of
F2(),
(FF . c) by A24;
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 A24, MSUALG_3:def 10;
:: 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 A24;
:: thesis: verum
end;
consider FofI1 being ManySortedSet of CC such that
A25:
for c being Element of CC holds S3[c,FofI1 . c]
from PBOOLE:sch 6(A23);
A26:
for c being Element of CC ex F1 being ManySortedFunction of F2(),(FF . c) st
( F1 = FofI1 . c & F1 is_homomorphism F2(),FF . c )
FofI1 is Function-yielding
then reconsider FofI1 = FofI1 as ManySortedFunction of CC ;
consider H being ManySortedFunction of F2(),(product FF) such that
A29:
H is_homomorphism F2(), product FF
and
A30:
for c being Element of CC holds (proj FF,c) ** H = FofI1 . c
by A26, PRALG_3:30;
A31:
QuotMSAlg F2(),(MSCng H), Image (MSHomQuot H) are_isomorphic
by A29, MSUALG_4:4, MSUALG_9:17;
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 . ithen reconsider s =
i as
SortSymbol of
F1() ;
consider Q being
Subset-Family of
([|the Sorts of F2(),the Sorts of F2()|] . s) such that A32:
Q = |:CC:| . s
and A33:
(meet |:CC:|) . s = Intersect Q
by MSSUBFAM:def 2;
A34:
|:CC:| . s = { (t . s) where t is Element of Bool [|the Sorts of F2(),the Sorts of F2()|] : t in CC }
by CLOSURE2:15;
(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 A35:
[a,b] in (MSCng H) . s
;
:: thesis: [a,b] in R0 . sthen A36:
(
a in the
Sorts of
F2()
. s &
b in the
Sorts of
F2()
. s )
by ZFMISC_1:106;
[a,b] in [:(the Sorts of F2() . s),(the Sorts of F2() . s):]
by A35;
then A37:
[a,b] in [|the Sorts of F2(),the Sorts of F2()|] . s
by PBOOLE:def 21;
A38:
[a,b] in MSCng H,
s
by A29, A35, MSUALG_4:def 20;
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 A39:
Y = t . s
and A40:
t in CC
by A32, A34;
reconsider t1 =
t as
Element of
CC by A40;
consider F1 being
ManySortedFunction of
F2(),
(FF . t1) such that A41:
(
F1 = FofI1 . t1 &
F1 is_homomorphism F2(),
FF . t1 & ex
R being
MSCongruence of
F2() st
(
t1 = R &
F1 = MSNat_Hom F2(),
R ) )
by A25;
consider R being
MSCongruence of
F2()
such that A42:
(
t1 = R &
F1 = MSNat_Hom F2(),
R )
by A41;
(F1 . s) . a =
(((proj FF,t1) ** H) . s) . a
by A30, A41
.=
(((proj FF,t1) . s) * (H . s)) . a
by MSUALG_3:2
.=
((proj FF,t1) . s) . ((H . s) . a)
by A36, FUNCT_2:21
.=
((proj FF,t1) . s) . ((H . s) . b)
by A36, A38, MSUALG_4:def 19
.=
(((proj FF,t1) . s) * (H . s)) . b
by A36, FUNCT_2:21
.=
(((proj FF,t1) ** H) . s) . b
by MSUALG_3:2
.=
(F1 . s) . b
by A30, A41
;
hence
[a,b] in Y
by A36, A39, A42, MSUALG_9:34;
:: thesis: verum
end; hence
[a,b] in R0 . s
by A33, A37, SETFAM_1:58;
:: thesis: verum
end;
assume A43:
[a,b] in R0 . s
;
:: thesis: [a,b] in (MSCng H) . s
then A44:
(
a in the
Sorts of
F2()
. s &
b in the
Sorts of
F2()
. s )
by ZFMISC_1:106;
then
(H . s) . a in the
Sorts of
(product FF) . s
by FUNCT_2:7;
then A45:
(H . s) . a in product (Carrier FF,s)
by PRALG_2:def 17;
(H . s) . b in the
Sorts of
(product FF) . s
by A44, FUNCT_2:7;
then A46:
(H . s) . b in product (Carrier FF,s)
by PRALG_2:def 17;
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 A5;
t1 is
Element of
Bool [|the Sorts of F2(),the Sorts of F2()|]
by CLOSURE2:def 1;
then
t1 . s in |:CC:| . s
by A34;
then A47:
[a,b] in t1 . s
by A32, A33, A43, SETFAM_1:58;
consider F1 being
ManySortedFunction of
F2(),
(FF . c) such that A48:
(
F1 = FofI1 . c &
F1 is_homomorphism F2(),
FF . c & ex
R being
MSCongruence of
F2() st
(
c = R &
F1 = MSNat_Hom F2(),
R ) )
by A25;
consider R being
MSCongruence of
F2()
such that A49:
(
t1 = R &
F1 = MSNat_Hom F2(),
R )
by A48;
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 A44, FUNCT_2:21
.=
(((proj FF,c) ** H) . s) . a
by MSUALG_3:2
.=
(F1 . s) . a
by A30, A48
.=
(F1 . s) . b
by A44, A47, A49, MSUALG_9:34
.=
(((proj FF,c) ** H) . s) . b
by A30, A48
.=
(((proj FF,c) . s) * (H . s)) . b
by MSUALG_3:2
.=
((proj FF,c) . s) . ((H . s) . b)
by A44, FUNCT_2:21
.=
(proj (Carrier FF,s),c) . ((H . s) . b)
by PRALG_3:def 3
;
:: thesis: verum
end;
then
(H . s) . a = (H . s) . b
by A45, A46, MSUALG_9:15;
then
[a,b] in MSCng H,
s
by A44, MSUALG_4:def 19;
hence
[a,b] in (MSCng H) . s
by A29, MSUALG_4:def 20;
:: thesis: verum
end; hence
(MSCng H) . i = R0 . i
;
:: thesis: verum end;
then
MSCng H = R0
by PBOOLE:3;
then consider XX being strict non-empty MSSubAlgebra of product FF such that
A50:
A,XX are_isomorphic
by A31;
P1[XX]
by A2, A22;
hence
P1[A]
by A1, A50, 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 A51:
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 ) )
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
A52:
G is_homomorphism F2(),B
and
A53:
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 ;
A54:
QuotMSAlg F2(),(MSCng G),C are_isomorphic
by A52, MSUALG_4:4, MSUALG_9:17;
A55:
MSCng G is Element of (CongrLatt F2())
by MSUALG_5:def 6;
P1[C]
by A2, A53;
then
P1[ QuotMSAlg F2(),(MSCng G)]
by A1, A54, MSUALG_3:17;
then
MSCng G in CC
by A55;
then
R0 c= MSCng G
by CLOSURE2:22, MSSUBFAM:43;
then consider H being ManySortedFunction of A,B such that
A56:
( H is_homomorphism A,B & G = H ** F )
by A52, MSUALG_9:37;
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 A56; :: 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 A57:
K ** F = G
; :: thesis: H = K
F is "onto"
by A51, MSUALG_3:def 10;
hence
H = K
by A56, A57, EXTENS_1:16; :: thesis: verum