consider G being GeneratorSet of A such that
A1: G is finite-yielding by MSAFREE2:def 10;
consider B being ManySortedSet of the carrier of S such that
A2: B in the Sorts of A by PBOOLE:134;
deffunc H₁( object ) -> set = {(B . S)};
consider C being ManySortedSet of the carrier of S such that
A3: for i being object st i in the carrier of S holds
C . i = H₁(i) from PBOOLE:sch 4();
set H = G (\/) C;

now :: thesis: for i being object st i in the carrier of S holds
C . i c= the Sorts of A . i

let i be object ; :: thesis: ( i in the carrier of S implies C . i c= the Sorts of A . i )
assume A4: i in the carrier of S ; :: thesis: C . i c= the Sorts of A . i
then B . i in the Sorts of A . i by A2;
then {(B . i)} c= the Sorts of A . i by ZFMISC_1:31;
hence C . i c= the Sorts of A . i by A3, A4; :: thesis: verum

end;

then ( G c= the Sorts of A & C c= the Sorts of A ) by PBOOLE:def 18;
then A5: ( C c= G (\/) C & G (\/) C c= the Sorts of A ) by PBOOLE:14, PBOOLE:16;

now :: thesis: for i being object st i in the carrier of S holds
not C . i is empty

let i be object ; :: thesis: ( i in the carrier of S implies not C . i is empty )
assume i in the carrier of S ; :: thesis: not C . i is empty
then C . i = {(B . i)} by A3;
hence not C . i is empty ; :: thesis: verum

end;

then C is non-empty ;
then reconsider H = G (\/) C as non-empty MSSubset of A by A5, PBOOLE:131, PBOOLE:def 18;
G c= H by PBOOLE:14;
then reconsider H = H as GeneratorSet of A by Th20;
take H ; :: thesis: ( H is non-empty & H is finite-yielding )
thus H is non-empty ; :: thesis: H is finite-yielding
let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in the carrier of S or H . i is finite )
assume A6: i in the carrier of S ; :: thesis: H . i is finite
then A7: C . i = {(B . i)} by A3;
A8: H . i = (G . i) \/ (C . i) by A6, PBOOLE:def 4;
G . i is finite by A1;
hence H . i is finite by A7, A8; :: thesis: verum