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

A4: F_{4}() .:.: F_{2}() is V2()
_{4}() .:.: F_{2}() is ManySortedSubset of the Sorts of F_{3}()
_{4}() .:.: F_{2}() as V2() MSSubset of F_{3}() by A4;

set AA = GenMSAlg Gen;

A9: F_{2}() is_transformable_to the Sorts of (GenMSAlg Gen)
;

F_{2}() is_transformable_to the Sorts of F_{3}()
;

then A10: doms F_{4}() = F_{2}()
by MSSUBFAM:17;

then rngs F_{4}() = F_{4}() .:.: F_{2}()
by EQUATION:13;

then rngs F_{4}() is ManySortedSubset of the Sorts of (GenMSAlg Gen)
by MSUALG_2:def 17;

then rngs F_{4}() c= the Sorts of (GenMSAlg Gen)
by PBOOLE:def 18;

then reconsider iN = F_{4}() as ManySortedFunction of F_{2}(), the Sorts of (GenMSAlg Gen) by A9, A10, EQUATION:4;

consider IN being ManySortedFunction of F_{3}(),(GenMSAlg Gen) such that

A11: IN is_homomorphism F_{3}(), GenMSAlg Gen
and

A12: IN ** F_{4}() = iN
and

for K being ManySortedFunction of F_{3}(),(GenMSAlg Gen) st K is_homomorphism F_{3}(), GenMSAlg Gen & K ** F_{4}() = iN holds

IN = K by A1, A2, A3;

the Sorts of (GenMSAlg Gen) is ManySortedSubset of the Sorts of F_{3}()
by MSUALG_2:def 9;

then reconsider h = id the Sorts of (GenMSAlg Gen) as ManySortedFunction of (GenMSAlg Gen),F_{3}() by EXTENS_1:5;

consider HIN being ManySortedFunction of F_{3}(),F_{3}() such that

HIN is_homomorphism F_{3}(),F_{3}()
and

HIN ** F_{4}() = h ** iN
and

A13: for K being ManySortedFunction of F_{3}(),F_{3}() st K is_homomorphism F_{3}(),F_{3}() & K ** F_{4}() = h ** iN holds

HIN = K by A1, A2;

h is_monomorphism GenMSAlg Gen,F_{3}()
by MSUALG_3:22;

then A14: h is_homomorphism GenMSAlg Gen,F_{3}()
by MSUALG_3:def 9;

reconsider hIN = h ** IN as ManySortedFunction of F_{3}(),F_{3}() ;

h ** iN = (h ** IN) ** F_{4}()
by A12, PBOOLE:140;

then A15: HIN = hIN by A11, A13, A14, MSUALG_3:10;

A16: F_{3}() is MSSubAlgebra of F_{3}()
by MSUALG_2:5;

F_{4}() = h ** iN
by MSUALG_3:4;

then (id the Sorts of F_{3}()) ** F_{4}() = h ** iN
by MSUALG_3:4;

then HIN = id the Sorts of F_{3}()
by A13, MSUALG_3:9;

then A17: HIN is "onto" ;

the Sorts of (GenMSAlg Gen) = h .:.: the Sorts of (GenMSAlg Gen) by EQUATION:15

.= the Sorts of F_{3}()
by A15, A17, EQUATION:2, EQUATION:9
;

then GenMSAlg Gen = F_{3}()
by A16, MSUALG_2:9;

hence F_{4}() .:.: F_{2}() is V2() GeneratorSet of F_{3}()
by MSAFREE:3; :: thesis: verum

A4: F

proof

F
let i be object ; :: according to PBOOLE:def 13 :: thesis: ( not i in the carrier of F_{1}() or not (F_{4}() .:.: F_{2}()) . i is empty )

assume A5: i in the carrier of F_{1}()
; :: thesis: not (F_{4}() .:.: F_{2}()) . i is empty

then reconsider fi = F_{4}() . i as Function of (F_{2}() . i),( the Sorts of F_{3}() . i) by PBOOLE:def 15;

A6: (F_{4}() .:.: F_{2}()) . i = fi .: (F_{2}() . i)
by A5, PBOOLE:def 20;

reconsider Xi = F_{2}() . i as non empty set by A5;

A7: Xi meets Xi ;

dom fi = Xi by A5, FUNCT_2:def 1;

hence not (F_{4}() .:.: F_{2}()) . i is empty
by A7, A6, RELAT_1:118; :: thesis: verum

end;assume A5: i in the carrier of F

then reconsider fi = F

A6: (F

reconsider Xi = F

A7: Xi meets Xi ;

dom fi = Xi by A5, FUNCT_2:def 1;

hence not (F

proof

then reconsider Gen = F
let i be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not i in the carrier of F_{1}() or (F_{4}() .:.: F_{2}()) . i c= the Sorts of F_{3}() . i )

assume A8: i in the carrier of F_{1}()
; :: thesis: (F_{4}() .:.: F_{2}()) . i c= the Sorts of F_{3}() . i

then reconsider fi = F_{4}() . i as Function of (F_{2}() . i),( the Sorts of F_{3}() . i) by PBOOLE:def 15;

(F_{4}() .:.: F_{2}()) . i = fi .: (F_{2}() . i)
by A8, PBOOLE:def 20;

hence (F_{4}() .:.: F_{2}()) . i c= the Sorts of F_{3}() . i
; :: thesis: verum

end;assume A8: i in the carrier of F

then reconsider fi = F

(F

hence (F

set AA = GenMSAlg Gen;

A9: F

F

then A10: doms F

then rngs F

then rngs F

then rngs F

then reconsider iN = F

consider IN being ManySortedFunction of F

A11: IN is_homomorphism F

A12: IN ** F

for K being ManySortedFunction of F

IN = K by A1, A2, A3;

the Sorts of (GenMSAlg Gen) is ManySortedSubset of the Sorts of F

then reconsider h = id the Sorts of (GenMSAlg Gen) as ManySortedFunction of (GenMSAlg Gen),F

consider HIN being ManySortedFunction of F

HIN is_homomorphism F

HIN ** F

A13: for K being ManySortedFunction of F

HIN = K by A1, A2;

h is_monomorphism GenMSAlg Gen,F

then A14: h is_homomorphism GenMSAlg Gen,F

reconsider hIN = h ** IN as ManySortedFunction of F

h ** iN = (h ** IN) ** F

then A15: HIN = hIN by A11, A13, A14, MSUALG_3:10;

A16: F

F

then (id the Sorts of F

then HIN = id the Sorts of F

then A17: HIN is "onto" ;

the Sorts of (GenMSAlg Gen) = h .:.: the Sorts of (GenMSAlg Gen) by EQUATION:15

.= the Sorts of F

then GenMSAlg Gen = F

hence F