let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for Y being infinite-yielding ManySortedSet of the carrier of S
for A being finite Subset of (Union the Sorts of (Free (S,Y))) ex y being Element of Y . s st
for v being Element of (Free (S,Y)) st v in A holds
v is y -omitting
let s be SortSymbol of S; :: thesis: for Y being infinite-yielding ManySortedSet of the carrier of S
for A being finite Subset of (Union the Sorts of (Free (S,Y))) ex y being Element of Y . s st
for v being Element of (Free (S,Y)) st v in A holds
v is y -omitting
let Y be infinite-yielding ManySortedSet of the carrier of S; :: thesis: for A being finite Subset of (Union the Sorts of (Free (S,Y))) ex y being Element of Y . s st
for v being Element of (Free (S,Y)) st v in A holds
v is y -omitting
let A be finite Subset of (Union the Sorts of (Free (S,Y))); :: thesis: ex y being Element of Y . s st
for v being Element of (Free (S,Y)) st v in A holds
v is y -omitting
set I = union { (vf v) where v is Element of (Free (S,Y)) : v in A } ;
A0: A is finite ;
deffunc H₁( Element of (Free (S,Y))) -> set = vf $1;
A1: { H₁(v) where v is Element of (Free (S,Y)) : v in A } is finite from FRAENKEL:sch 21(A0);

now :: thesis: for a being set st a in { H₁(v) where v is Element of (Free (S,Y)) : v in A } holds
a is finite

let a be set ; :: thesis: ( a in { H₁(v) where v is Element of (Free (S,Y)) : v in A } implies a is finite )
assume a in { H₁(v) where v is Element of (Free (S,Y)) : v in A } ; :: thesis: a is finite
then ex v being Element of (Free (S,Y)) st
( a = H₁(v) & v in A ) ;
hence a is finite ; :: thesis: verum

end;

then reconsider I = union { (vf v) where v is Element of (Free (S,Y)) : v in A } as finite set by A1, FINSET_1:7;
set y = the Element of (Y . s) \ I;
reconsider y = the Element of (Y . s) \ I as Element of Y . s ;
take y ; :: thesis: for v being Element of (Free (S,Y)) st v in A holds
v is y -omitting
let v be Element of (Free (S,Y)); :: thesis: ( v in A implies v is y -omitting )
assume v in A ; :: thesis: v is y -omitting
then H₁(v) in { H₁(v1) where v1 is Element of (Free (S,Y)) : v1 in A } ;
then ( y nin I & H₁(v) c= I ) by XBOOLE_0:def 5, ZFMISC_1:74;
hence v is y -omitting by Th92; :: thesis: verum