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

now

let i be set ; :: 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 A4: C is non-empty by PBOOLE:def 16;
set H = G \/ C;
A5: C c= G \/ C by PBOOLE:16;
A6: G c= the Sorts of A by PBOOLE:def 23;

now

let i be set ; :: thesis: ( i in the carrier of S implies C . i c= the Sorts of A . i )
assume A7: 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, PBOOLE:def 4;
then {(B . i)} c= the Sorts of A . i by ZFMISC_1:37;
hence C . i c= the Sorts of A . i by A3, A7; :: thesis: verum

end;

then C c= the Sorts of A by PBOOLE:def 5;
then G \/ C c= the Sorts of A by A6, PBOOLE:18;
then reconsider H = G \/ C as V2 MSSubset of A by A4, A5, PBOOLE:143, PBOOLE:def 23;
G c= H by PBOOLE:16;
then reconsider H = H as GeneratorSet of A by Th21;
take H ; :: thesis: ( H is non-empty & H is locally-finite )
thus H is non-empty ; :: thesis: H is locally-finite
let i be set ; :: according to PRE_CIRC:def 3 :: thesis: ( not i in the carrier of S or H . i is finite )
assume A8: i in the carrier of S ; :: thesis: H . i is finite
then A9: G . i is finite by A1, PRE_CIRC:def 3;
A10: C . i = {(B . i)} by A3, A8;
H . i = (G . i) \/ (C . i) by A8, PBOOLE:def 7;
hence H . i is finite by A9, A10; :: thesis: verum