set I = the carrier of F1();
A4: F4() .:.: F2() is V2()
proof
let i be object ; :: according to PBOOLE:def 13 :: thesis: ( not i in the carrier of F1() or not (F4() .:.: F2()) . i is empty )
assume A5: i in the carrier of F1() ; :: thesis: not (F4() .:.: F2()) . i is empty
then reconsider fi = F4() . i as Function of (F2() . i),( the Sorts of F3() . i) by PBOOLE:def 15;
A6: (F4() .:.: F2()) . i = fi .: (F2() . i) by ;
reconsider Xi = F2() . i as non empty set by A5;
A7: Xi meets Xi ;
dom fi = Xi by ;
hence not (F4() .:.: F2()) . i is empty by ; :: thesis: verum
end;
F4() .:.: F2() is ManySortedSubset of the Sorts of F3()
proof
let i be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not i in the carrier of F1() or (F4() .:.: F2()) . i c= the Sorts of F3() . i )
assume A8: i in the carrier of F1() ; :: thesis: (F4() .:.: F2()) . i c= the Sorts of F3() . i
then reconsider fi = F4() . i as Function of (F2() . i),( the Sorts of F3() . i) by PBOOLE:def 15;
(F4() .:.: F2()) . i = fi .: (F2() . i) by ;
hence (F4() .:.: F2()) . i c= the Sorts of F3() . i ; :: thesis: verum
end;
then reconsider Gen = F4() .:.: F2() as V2() MSSubset of F3() by A4;
set AA = GenMSAlg Gen;
A9: F2() is_transformable_to the Sorts of (GenMSAlg Gen) ;
F2() is_transformable_to the Sorts of F3() ;
then A10: doms F4() = F2() by MSSUBFAM:17;
then rngs F4() = F4() .:.: F2() by EQUATION:13;
then rngs F4() is ManySortedSubset of the Sorts of (GenMSAlg Gen) by MSUALG_2:def 17;
then rngs F4() c= the Sorts of (GenMSAlg Gen) by PBOOLE:def 18;
then reconsider iN = F4() as ManySortedFunction of F2(), the Sorts of (GenMSAlg Gen) by ;
consider IN being ManySortedFunction of F3(),(GenMSAlg Gen) such that
A11: IN is_homomorphism F3(), GenMSAlg Gen and
A12: IN ** F4() = iN and
for K being ManySortedFunction of F3(),(GenMSAlg Gen) st K is_homomorphism F3(), GenMSAlg Gen & K ** F4() = iN holds
IN = K by A1, A2, A3;
the Sorts of (GenMSAlg Gen) is ManySortedSubset of the Sorts of F3() by MSUALG_2:def 9;
then reconsider h = id the Sorts of (GenMSAlg Gen) as ManySortedFunction of (GenMSAlg Gen),F3() by EXTENS_1:5;
consider HIN being ManySortedFunction of F3(),F3() such that
HIN is_homomorphism F3(),F3() and
HIN ** F4() = h ** iN and
A13: for K being ManySortedFunction of F3(),F3() st K is_homomorphism F3(),F3() & K ** F4() = h ** iN holds
HIN = K by A1, A2;
h is_monomorphism GenMSAlg Gen,F3() by MSUALG_3:22;
then A14: h is_homomorphism GenMSAlg Gen,F3() by MSUALG_3:def 9;
reconsider hIN = h ** IN as ManySortedFunction of F3(),F3() ;
h ** iN = (h ** IN) ** F4() by ;
then A15: HIN = hIN by ;
A16: F3() is MSSubAlgebra of F3() by MSUALG_2:5;
F4() = h ** iN by MSUALG_3:4;
then (id the Sorts of F3()) ** F4() = h ** iN by MSUALG_3:4;
then HIN = id the Sorts of F3() by ;
then A17: HIN is "onto" ;
the Sorts of (GenMSAlg Gen) = h .:.: the Sorts of (GenMSAlg Gen) by EQUATION:15
.= the Sorts of F3() by ;
then GenMSAlg Gen = F3() by ;
hence F4() .:.: F2() is V2() GeneratorSet of F3() by MSAFREE:3; :: thesis: verum