theorem Th9: :: ZF_FUND1:9

for V being Universe
for a 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 X holds
Funcs (fs,a) in X