set EMF = the MSAlgebra-Family of {} ,F_{1}();

set CC = { C where C is Element of (CongrLatt F_{2}()) : ex R being MSCongruence of F_{2}() st

( R = C & P_{1}[ QuotMSAlg (F_{2}(),R)] ) } ;

set SF = the Sorts of F_{2}();

set I = the carrier of F_{1}();

consider Xi being ManySortedSet of the carrier of F_{1}() such that

A4: {Xi} = the carrier of F_{1}() --> {{}}
by MSUALG_9:5;

_{1}()) = {Xi}
;

reconsider R = [| the Sorts of F_{2}(), the Sorts of F_{2}()|] as MSCongruence of F_{2}() by MSUALG_5:18;

[| the Sorts of F_{2}(), the Sorts of F_{2}()|] is MSCongruence of F_{2}()
by MSUALG_5:18;

then A6: [| the Sorts of F_{2}(), the Sorts of F_{2}()|] is Element of (CongrLatt F_{2}())
by MSUALG_5:def 6;

the Sorts of (QuotMSAlg (F_{2}(),R)) = { the Sorts of F_{2}()}
by MSUALG_9:29;

then A7: QuotMSAlg (F_{2}(),R), Trivial_Algebra F_{1}() are_isomorphic
by MSUALG_9:26;

for i being set st i in {} holds

ex A being MSAlgebra over F_{1}() st

( A = the MSAlgebra-Family of {} ,F_{1}() . i & P_{1}[A] )
;

then P_{1}[ product the MSAlgebra-Family of {} ,F_{1}()]
by A3;

then P_{1}[ Trivial_Algebra F_{1}()]
by A1, A5, MSUALG_9:26;

then P_{1}[ QuotMSAlg (F_{2}(),R)]
by A1, A7, MSUALG_3:17;

then A8: [| the Sorts of F_{2}(), the Sorts of F_{2}()|] in { C where C is Element of (CongrLatt F_{2}()) : ex R being MSCongruence of F_{2}() st

( R = C & P_{1}[ QuotMSAlg (F_{2}(),R)] ) }
by A6;

defpred S_{1}[ object , object ] means ex R being MSCongruence of F_{2}() st

( R = $1 & $2 = QuotMSAlg (F_{2}(),R) );

defpred S_{2}[ set ] means ex R being MSCongruence of F_{2}() st

( R = $1 & P_{1}[ QuotMSAlg (F_{2}(),R)] );

_{2}()) : ex R being MSCongruence of F_{2}() st

( R = C & P_{1}[ QuotMSAlg (F_{2}(),R)] ) } c= the carrier of (EqRelLatt the Sorts of F_{2}())
_{2}()) : ex R being MSCongruence of F_{2}() st

( R = C & P_{1}[ QuotMSAlg (F_{2}(),R)] ) } as non empty SubsetFamily of [| the Sorts of F_{2}(), the Sorts of F_{2}()|] by A8, MSUALG_7:5;

set R0 = meet |:CC:|;

A11: meet |:CC:| is MSEquivalence_Relation-like ManySortedRelation of the Sorts of F_{2}()
by A10, MSUALG_7:8;

reconsider R0 = meet |:CC:| as ManySortedRelation of F_{2}() by A10, MSUALG_7:8;

R0 is MSEquivalence-like by A11;

then reconsider R0 = R0 as MSEquivalence-like ManySortedRelation of F_{2}() ;

{ C where C is Element of (CongrLatt F_{2}()) : S_{2}[C] } is Subset of (CongrLatt F_{2}())
from DOMAIN_1:sch 7();

then reconsider R0 = R0 as MSCongruence of F_{2}() by MSUALG_9:28;

take A = QuotMSAlg (F_{2}(),R0); :: thesis: ex F being ManySortedFunction of F_{2}(),A st

( P_{1}[A] & F is_epimorphism F_{2}(),A & ( for B being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of F_{2}(),B st G is_homomorphism F_{2}(),B & P_{1}[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 (F_{2}(),R0) as ManySortedFunction of F_{2}(),A ;

take F ; :: thesis: ( P_{1}[A] & F is_epimorphism F_{2}(),A & ( for B being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of F_{2}(),B st G is_homomorphism F_{2}(),B & P_{1}[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 ) ) ) )

A13: for c being object st c in CC holds

S_{1}[c,FF . c]
from PBOOLE:sch 3(A12);

FF is MSAlgebra-Family of CC,F_{1}()
_{1}() ;

defpred S_{3}[ Element of CC, object ] means ex F1 being ManySortedFunction of F_{2}(),(FF . $1) st

( F1 = $2 & F1 is_homomorphism F_{2}(),FF . $1 & ex R being MSCongruence of F_{2}() st

( $1 = R & F1 = MSNat_Hom (F_{2}(),R) ) );

A14: for c being Element of CC ex j being object st S_{3}[c,j]

A17: for c being Element of CC holds S_{3}[c,FofI1 . c]
from PBOOLE:sch 6(A14);

A18: for c being Element of CC ex F1 being ManySortedFunction of F_{2}(),(FF . c) st

( F1 = FofI1 . c & F1 is_homomorphism F_{2}(),FF . c )

consider H being ManySortedFunction of F_{2}(),(product FF) such that

A21: H is_homomorphism F_{2}(), product FF
and

A22: for c being Element of CC holds (proj (FF,c)) ** H = FofI1 . c by A18, PRALG_3:29;

QuotMSAlg (F_{2}(),(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_{1}() st

( A = FF . cc & P_{1}[A] )
_{1}[XX]
by A2, A3;

hence P_{1}[A]
by A1, A44, MSUALG_3:17; :: thesis: ( F is_epimorphism F_{2}(),A & ( for B being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of F_{2}(),B st G is_homomorphism F_{2}(),B & P_{1}[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 F_{2}(),A
by MSUALG_4:3; :: thesis: for B being non-empty MSAlgebra over F_{1}()

for G being ManySortedFunction of F_{2}(),B st G is_homomorphism F_{2}(),B & P_{1}[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 F_{1}(); :: thesis: for G being ManySortedFunction of F_{2}(),B st G is_homomorphism F_{2}(),B & P_{1}[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 F_{2}(),B; :: thesis: ( G is_homomorphism F_{2}(),B & P_{1}[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 F_{2}(),B
and

A49: P_{1}[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 ;

A50: QuotMSAlg (F_{2}(),(MSCng G)),C are_isomorphic
by A48, MSUALG_4:4, MSUALG_9:16;

A51: MSCng G is Element of (CongrLatt F_{2}())
by MSUALG_5:def 6;

P_{1}[C]
by A2, A49;

then P_{1}[ QuotMSAlg (F_{2}(),(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: ( 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 A53, A47, EXTENS_1:12; :: thesis: verum

set CC = { C where C is Element of (CongrLatt F

( R = C & P

set SF = the Sorts of F

set I = the carrier of F

consider Xi being ManySortedSet of the carrier of F

A4: {Xi} = the carrier of F

now :: thesis: for i being object st i in the carrier of F_{1}() holds

the Sorts of (product the MSAlgebra-Family of {} ,F_{1}()) . i = {Xi} . i

then A5:
the Sorts of (product the MSAlgebra-Family of {} ,Fthe Sorts of (product the MSAlgebra-Family of {} ,F

let i be object ; :: thesis: ( i in the carrier of F_{1}() implies the Sorts of (product the MSAlgebra-Family of {} ,F_{1}()) . i = {Xi} . i )

assume i in the carrier of F_{1}()
; :: thesis: the Sorts of (product the MSAlgebra-Family of {} ,F_{1}()) . i = {Xi} . i

then reconsider s = i as SortSymbol of F_{1}() ;

thus the Sorts of (product the MSAlgebra-Family of {} ,F_{1}()) . i =
product (Carrier ( the MSAlgebra-Family of {} ,F_{1}(),s))
by PRALG_2:def 10

.= {{}} by CARD_3:10, PRALG_2:def 9

.= ( the carrier of F_{1}() --> {{}}) . s

.= {Xi} . i by A4 ; :: thesis: verum

end;assume i in the carrier of F

then reconsider s = i as SortSymbol of F

thus the Sorts of (product the MSAlgebra-Family of {} ,F

.= {{}} by CARD_3:10, PRALG_2:def 9

.= ( the carrier of F

.= {Xi} . i by A4 ; :: thesis: verum

reconsider R = [| the Sorts of F

[| the Sorts of F

then A6: [| the Sorts of F

the Sorts of (QuotMSAlg (F

then A7: QuotMSAlg (F

for i being set st i in {} holds

ex A being MSAlgebra over F

( A = the MSAlgebra-Family of {} ,F

then P

then P

then P

then A8: [| the Sorts of F

( R = C & P

defpred S

( R = $1 & $2 = QuotMSAlg (F

defpred S

( R = $1 & P

A9: now :: thesis: for q being object st q in { C where C is Element of (CongrLatt F_{2}()) : ex R being MSCongruence of F_{2}() st

( R = C & P_{1}[ QuotMSAlg (F_{2}(),R)] ) } holds

q is MSCongruence of F_{2}()

A10:
{ C where C is Element of (CongrLatt F( R = C & P

q is MSCongruence of F

let q be object ; :: thesis: ( q in { C where C is Element of (CongrLatt F_{2}()) : ex R being MSCongruence of F_{2}() st

( R = C & P_{1}[ QuotMSAlg (F_{2}(),R)] ) } implies q is MSCongruence of F_{2}() )

assume q in { C where C is Element of (CongrLatt F_{2}()) : ex R being MSCongruence of F_{2}() st

( R = C & P_{1}[ QuotMSAlg (F_{2}(),R)] ) }
; :: thesis: q is MSCongruence of F_{2}()

then ex C being Element of (CongrLatt F_{2}()) st

( q = C & ex R being MSCongruence of F_{2}() st

( R = C & P_{1}[ QuotMSAlg (F_{2}(),R)] ) )
;

hence q is MSCongruence of F_{2}()
; :: thesis: verum

end;( R = C & P

assume q in { C where C is Element of (CongrLatt F

( R = C & P

then ex C being Element of (CongrLatt F

( q = C & ex R being MSCongruence of F

( R = C & P

hence q is MSCongruence of F

( R = C & P

proof

then reconsider CC = { C where C is Element of (CongrLatt F
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { C where C is Element of (CongrLatt F_{2}()) : ex R being MSCongruence of F_{2}() st

( R = C & P_{1}[ QuotMSAlg (F_{2}(),R)] ) } or q in the carrier of (EqRelLatt the Sorts of F_{2}()) )

assume q in { C where C is Element of (CongrLatt F_{2}()) : ex R being MSCongruence of F_{2}() st

( R = C & P_{1}[ QuotMSAlg (F_{2}(),R)] ) }
; :: thesis: q in the carrier of (EqRelLatt the Sorts of F_{2}())

then q is Equivalence_Relation of the Sorts of F_{2}()
by A9;

hence q in the carrier of (EqRelLatt the Sorts of F_{2}())
by MSUALG_5:def 5; :: thesis: verum

end;( R = C & P

assume q in { C where C is Element of (CongrLatt F

( R = C & P

then q is Equivalence_Relation of the Sorts of F

hence q in the carrier of (EqRelLatt the Sorts of F

( R = C & P

set R0 = meet |:CC:|;

A11: meet |:CC:| is MSEquivalence_Relation-like ManySortedRelation of the Sorts of F

reconsider R0 = meet |:CC:| as ManySortedRelation of F

R0 is MSEquivalence-like by A11;

then reconsider R0 = R0 as MSEquivalence-like ManySortedRelation of F

{ C where C is Element of (CongrLatt F

then reconsider R0 = R0 as MSCongruence of F

take A = QuotMSAlg (F

( P

for G being ManySortedFunction of F

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 (F

take F ; :: thesis: ( P

for G being ManySortedFunction of F

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 S_{1}[c,w]

consider FF being ManySortedSet of CC such that ex w being object st S

let c be object ; :: thesis: ( c in CC implies ex w being object st S_{1}[c,w] )

assume c in CC ; :: thesis: ex w being object st S_{1}[c,w]

then reconsider cc = c as MSCongruence of F_{2}() by A9;

reconsider w = QuotMSAlg (F_{2}(),cc) as object ;

take w = w; :: thesis: S_{1}[c,w]

thus S_{1}[c,w]
; :: thesis: verum

end;assume c in CC ; :: thesis: ex w being object st S

then reconsider cc = c as MSCongruence of F

reconsider w = QuotMSAlg (F

take w = w; :: thesis: S

thus S

A13: for c being object st c in CC holds

S

FF is MSAlgebra-Family of CC,F

proof

then reconsider FF = FF as MSAlgebra-Family of CC,F
let c be object ; :: according to PRALG_2:def 5 :: thesis: ( not c in CC or FF . c is MSAlgebra over F_{1}() )

assume c in CC ; :: thesis: FF . c is MSAlgebra over F_{1}()

then ex R being MSCongruence of F_{2}() st

( R = c & FF . c = QuotMSAlg (F_{2}(),R) )
by A13;

hence FF . c is MSAlgebra over F_{1}()
; :: thesis: verum

end;assume c in CC ; :: thesis: FF . c is MSAlgebra over F

then ex R being MSCongruence of F

( R = c & FF . c = QuotMSAlg (F

hence FF . c is MSAlgebra over F

defpred S

( F1 = $2 & F1 is_homomorphism F

( $1 = R & F1 = MSNat_Hom (F

A14: for c being Element of CC ex j being object st S

proof

consider FofI1 being ManySortedSet of CC such that
let c be Element of CC; :: thesis: ex j being object st S_{3}[c,j]

consider R being MSCongruence of F_{2}() such that

A15: R = c and

A16: FF . c = QuotMSAlg (F_{2}(),R)
by A13;

set j = MSNat_Hom (F_{2}(),R);

reconsider F1 = MSNat_Hom (F_{2}(),R) as ManySortedFunction of F_{2}(),(FF . c) by A16;

take MSNat_Hom (F_{2}(),R)
; :: thesis: S_{3}[c, MSNat_Hom (F_{2}(),R)]

take F1 ; :: thesis: ( F1 = MSNat_Hom (F_{2}(),R) & F1 is_homomorphism F_{2}(),FF . c & ex R being MSCongruence of F_{2}() st

( c = R & F1 = MSNat_Hom (F_{2}(),R) ) )

thus F1 = MSNat_Hom (F_{2}(),R)
; :: thesis: ( F1 is_homomorphism F_{2}(),FF . c & ex R being MSCongruence of F_{2}() st

( c = R & F1 = MSNat_Hom (F_{2}(),R) ) )

MSNat_Hom (F_{2}(),R) is_epimorphism F_{2}(), QuotMSAlg (F_{2}(),R)
by MSUALG_4:3;

hence F1 is_homomorphism F_{2}(),FF . c
by A16, MSUALG_3:def 8; :: thesis: ex R being MSCongruence of F_{2}() st

( c = R & F1 = MSNat_Hom (F_{2}(),R) )

take R ; :: thesis: ( c = R & F1 = MSNat_Hom (F_{2}(),R) )

thus ( c = R & F1 = MSNat_Hom (F_{2}(),R) )
by A15; :: thesis: verum

end;consider R being MSCongruence of F

A15: R = c and

A16: FF . c = QuotMSAlg (F

set j = MSNat_Hom (F

reconsider F1 = MSNat_Hom (F

take MSNat_Hom (F

take F1 ; :: thesis: ( F1 = MSNat_Hom (F

( c = R & F1 = MSNat_Hom (F

thus F1 = MSNat_Hom (F

( c = R & F1 = MSNat_Hom (F

MSNat_Hom (F

hence F1 is_homomorphism F

( c = R & F1 = MSNat_Hom (F

take R ; :: thesis: ( c = R & F1 = MSNat_Hom (F

thus ( c = R & F1 = MSNat_Hom (F

A17: for c being Element of CC holds S

A18: for c being Element of CC ex F1 being ManySortedFunction of F

( F1 = FofI1 . c & F1 is_homomorphism F

proof

FofI1 is Function-yielding
let c be Element of CC; :: thesis: ex F1 being ManySortedFunction of F_{2}(),(FF . c) st

( F1 = FofI1 . c & F1 is_homomorphism F_{2}(),FF . c )

consider F1 being ManySortedFunction of F_{2}(),(FF . c) such that

A19: F1 = FofI1 . c and

A20: F1 is_homomorphism F_{2}(),FF . c
and

ex R being MSCongruence of F_{2}() st

( c = R & F1 = MSNat_Hom (F_{2}(),R) )
by A17;

take F1 ; :: thesis: ( F1 = FofI1 . c & F1 is_homomorphism F_{2}(),FF . c )

thus ( F1 = FofI1 . c & F1 is_homomorphism F_{2}(),FF . c )
by A19, A20; :: thesis: verum

end;( F1 = FofI1 . c & F1 is_homomorphism F

consider F1 being ManySortedFunction of F

A19: F1 = FofI1 . c and

A20: F1 is_homomorphism F

ex R being MSCongruence of F

( c = R & F1 = MSNat_Hom (F

take F1 ; :: thesis: ( F1 = FofI1 . c & F1 is_homomorphism F

thus ( F1 = FofI1 . c & F1 is_homomorphism F

proof

then reconsider FofI1 = FofI1 as ManySortedFunction of CC ;
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 F_{2}(),(FF . cc) st

( F1 = FofI1 . cc & F1 is_homomorphism F_{2}(),FF . cc )
by A18;

hence FofI1 . c is set ; :: thesis: verum

end;assume c in dom FofI1 ; :: thesis: FofI1 . c is set

then reconsider cc = c as Element of CC ;

ex F1 being ManySortedFunction of F

( F1 = FofI1 . cc & F1 is_homomorphism F

hence FofI1 . c is set ; :: thesis: verum

consider H being ManySortedFunction of F

A21: H is_homomorphism F

A22: for c being Element of CC holds (proj (FF,c)) ** H = FofI1 . c by A18, PRALG_3:29;

now :: thesis: for i being object st i in the carrier of F_{1}() holds

(MSCng H) . i = R0 . i

then A43:
MSCng H = R0
;(MSCng H) . i = R0 . i

let i be object ; :: thesis: ( i in the carrier of F_{1}() implies (MSCng H) . i = R0 . i )

assume i in the carrier of F_{1}()
; :: thesis: (MSCng H) . i = R0 . i

then reconsider s = i as SortSymbol of F_{1}() ;

consider Q being Subset-Family of ([| the Sorts of F_{2}(), the Sorts of F_{2}()|] . 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_{2}(), the Sorts of F_{2}()|] : t in CC }
by CLOSURE2:14;

(MSCng H) . s = R0 . s

end;assume i in the carrier of F

then reconsider s = i as SortSymbol of F

consider Q being Subset-Family of ([| the Sorts of F

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

(MSCng H) . s = R0 . s

proof

hence
(MSCng H) . i = R0 . i
; :: thesis: verum
let a, b be object ; :: 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 ) )

then A36: a in the Sorts of F_{2}() . s
by ZFMISC_1:87;

A37: b in the Sorts of F_{2}() . 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)

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: verum

end;hereby :: thesis: ( not [a,b] in R0 . s or [a,b] in (MSCng H) . s )

assume A35:
[a,b] in R0 . s
; :: thesis: [a,b] in (MSCng H) . sassume A26:
[a,b] in (MSCng H) . s
; :: thesis: [a,b] in R0 . s

then A27: a in the Sorts of F_{2}() . s
by ZFMISC_1:87;

A28: b in the Sorts of F_{2}() . 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_{2}() . s),( the Sorts of F_{2}() . s):]
by A26;

then [a,b] in [| the Sorts of F_{2}(), the Sorts of F_{2}()|] . s
by PBOOLE:def 16;

hence [a,b] in R0 . s by A24, A30, SETFAM_1:43; :: thesis: verum

end;then A27: a in the Sorts of F

A28: b in the Sorts of F

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

[a,b] in [:( the Sorts of F
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 F_{2}(), the Sorts of F_{2}()|] 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_{2}(),(FF . t1) such that

A33: F1 = FofI1 . t1 and

F1 is_homomorphism F_{2}(),FF . t1
and

A34: ex R being MSCongruence of F_{2}() st

( t1 = R & F1 = MSNat_Hom (F_{2}(),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: verum

end;assume Y in Q ; :: thesis: [a,b] in Y

then consider t being Element of Bool [| the Sorts of F

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

A33: F1 = FofI1 . t1 and

F1 is_homomorphism F

A34: ex R being MSCongruence of F

( t1 = R & F1 = MSNat_Hom (F

(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: verum

then [a,b] in [| the Sorts of F

hence [a,b] in R0 . s by A24, A30, SETFAM_1:43; :: thesis: verum

then A36: a in the Sorts of F

A37: b in the Sorts of F

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

(H . s) . b in the Sorts of (product FF) . s
by A37, FUNCT_2:5;
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 F_{2}() by A9;

consider F1 being ManySortedFunction of F_{2}(),(FF . c) such that

A39: F1 = FofI1 . c and

F1 is_homomorphism F_{2}(),FF . c
and

A40: ex R being MSCongruence of F_{2}() st

( c = R & F1 = MSNat_Hom (F_{2}(),R) )
by A17;

t1 is Element of Bool [| the Sorts of F_{2}(), the Sorts of F_{2}()|]
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: verum

end;reconsider t1 = c as MSCongruence of F

consider F1 being ManySortedFunction of F

A39: F1 = FofI1 . c and

F1 is_homomorphism F

A40: ex R being MSCongruence of F

( c = R & F1 = MSNat_Hom (F

t1 is Element of Bool [| the Sorts of F

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: verum

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: verum

QuotMSAlg (F

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

( A = FF . cc & P

proof

then
P
let cc be set ; :: thesis: ( cc in CC implies ex A being MSAlgebra over F_{1}() st

( A = FF . cc & P_{1}[A] ) )

assume A45: cc in CC ; :: thesis: ex A being MSAlgebra over F_{1}() st

( A = FF . cc & P_{1}[A] )

then reconsider c = cc as Element of CC ;

take FF . c ; :: thesis: ( FF . c = FF . cc & P_{1}[FF . c] )

A46: ex C being Element of (CongrLatt F_{2}()) st

( cc = C & ex R being MSCongruence of F_{2}() st

( R = C & P_{1}[ QuotMSAlg (F_{2}(),R)] ) )
by A45;

ex R being MSCongruence of F_{2}() st

( R = cc & FF . cc = QuotMSAlg (F_{2}(),R) )
by A13, A45;

hence ( FF . c = FF . cc & P_{1}[FF . c] )
by A46; :: thesis: verum

end;( A = FF . cc & P

assume A45: cc in CC ; :: thesis: ex A being MSAlgebra over F

( A = FF . cc & P

then reconsider c = cc as Element of CC ;

take FF . c ; :: thesis: ( FF . c = FF . cc & P

A46: ex C being Element of (CongrLatt F

( cc = C & ex R being MSCongruence of F

( R = C & P

ex R being MSCongruence of F

( R = cc & FF . cc = QuotMSAlg (F

hence ( FF . c = FF . cc & P

hence P

for G being ManySortedFunction of F

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 F

for G being ManySortedFunction of F

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 F

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 F

( 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 F

A49: P

( 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 ;

A50: QuotMSAlg (F

A51: MSCng G is Element of (CongrLatt F

P

then P

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: ( 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 A53, A47, EXTENS_1:12; :: thesis: verum