theorem Th10: :: ZF_FUND1:10

for V being Universe
for a, b being Element of V
for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in Funcs (fs,omega) & b in X holds
{ (a (#) x) where x is Element of V : x in b } in X