set I = the carrier of F₁();
A4: F₄() .:.: F₂() is non-empty

proof

let i be object ; :: according to PBOOLE:def 13 :: thesis: ( not i in the carrier of F₁() or not (F₄() .:.: F₂()) . i is empty )
assume A5: i in the carrier of F₁() ; :: thesis: not (F₄() .:.: F₂()) . i is empty
then reconsider fi = F₄() . i as Function of (F₂() . i),( the Sorts of F₃() . i) by PBOOLE:def 15;
A6: (F₄() .:.: F₂()) . i = fi .: (F₂() . i) by A5, PBOOLE:def 20;
reconsider Xi = F₂() . i as non empty set by A5;
A7: Xi meets Xi ;
dom fi = Xi by A5, FUNCT_2:def 1;
hence not (F₄() .:.: F₂()) . i is empty by A7, A6, RELAT_1:118; :: thesis: verum

end;

F₄() .:.: F₂() is ManySortedSubset of the Sorts of F₃()

proof

let i be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not i in the carrier of F₁() or (F₄() .:.: F₂()) . i c= the Sorts of F₃() . i )
assume A8: i in the carrier of F₁() ; :: thesis: (F₄() .:.: F₂()) . i c= the Sorts of F₃() . i
then reconsider fi = F₄() . i as Function of (F₂() . i),( the Sorts of F₃() . i) by PBOOLE:def 15;
(F₄() .:.: F₂()) . i = fi .: (F₂() . i) by A8, PBOOLE:def 20;
hence (F₄() .:.: F₂()) . i c= the Sorts of F₃() . i ; :: thesis: verum

end;

then reconsider Gen = F₄() .:.: F₂() as non-empty MSSubset of F₃() by A4;
set AA = GenMSAlg Gen;
A9: F₂() is_transformable_to the Sorts of (GenMSAlg Gen) ;
F₂() is_transformable_to the Sorts of F₃() ;
then A10: doms F₄() = F₂() by MSSUBFAM:17;
then rngs F₄() = F₄() .:.: F₂() by EQUATION:13;
then rngs F₄() is ManySortedSubset of the Sorts of (GenMSAlg Gen) by MSUALG_2:def 17;
then rngs F₄() c= the Sorts of (GenMSAlg Gen) by PBOOLE:def 18;
then reconsider iN = F₄() as ManySortedFunction of F₂(), the Sorts of (GenMSAlg Gen) by A9, A10, EQUATION:4;
consider IN being ManySortedFunction of F₃(),(GenMSAlg Gen) such that
A11: IN is_homomorphism F₃(), GenMSAlg Gen and
A12: IN ** F₄() = iN and
for K being ManySortedFunction of F₃(),(GenMSAlg Gen) st K is_homomorphism F₃(), GenMSAlg Gen & K ** F₄() = iN holds
IN = K by A1, A2, A3;
the Sorts of (GenMSAlg Gen) is ManySortedSubset of the Sorts of F₃() by MSUALG_2:def 9;
then reconsider h = id the Sorts of (GenMSAlg Gen) as ManySortedFunction of (GenMSAlg Gen),F₃() by EXTENS_1:5;
consider HIN being ManySortedFunction of F₃(),F₃() such that
HIN is_homomorphism F₃(),F₃() and
HIN ** F₄() = h ** iN and
A13: for K being ManySortedFunction of F₃(),F₃() st K is_homomorphism F₃(),F₃() & K ** F₄() = h ** iN holds
HIN = K by A1, A2;
h is_monomorphism GenMSAlg Gen,F₃() by MSUALG_3:22;
then A14: h is_homomorphism GenMSAlg Gen,F₃() by MSUALG_3:def 9;
reconsider hIN = h ** IN as ManySortedFunction of F₃(),F₃() ;
h ** iN = (h ** IN) ** F₄() by A12, PBOOLE:140;
then A15: HIN = hIN by A11, A13, A14, MSUALG_3:10;
A16: F₃() is MSSubAlgebra of F₃() by MSUALG_2:5;
F₄() = h ** iN by MSUALG_3:4;
then (id the Sorts of F₃()) ** F₄() = h ** iN by MSUALG_3:4;
then HIN = id the Sorts of F₃() 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₃() by A15, A17, EQUATION:2, EQUATION:9 ;
then GenMSAlg Gen = F₃() by A16, MSUALG_2:9;
hence F₄() .:.: F₂() is non-empty GeneratorSet of F₃() by MSAFREE:3; :: thesis: verum