theorem Th11: :: ZF_FUND1:11

for V being Universe
for a, b being Element of V
for X being Subclass of V
for n being Element of omega
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & n in fs & a in X & b in X & b c= Funcs (fs,a) holds
{ x where x is Element of V : ( x in Funcs ((fs \ {n}),a) & ex u being set st {[n,u]} \/ x in b ) } in X