let V be Universe; :: thesis: for y being Element of V
for X being Subclass of V
for A being set
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & A c= X & y in Funcs fs,A holds
y in X
let y be Element of V; :: thesis: for X being Subclass of V
for A being set
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & A c= X & y in Funcs fs,A holds
y in X
let X be Subclass of V; :: thesis: for A being set
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & A c= X & y in Funcs fs,A holds
y in X
let A be set ; :: thesis: for fs being finite Subset of omega st X is closed_wrt_A1-A7 & A c= X & y in Funcs fs,A holds
y in X
let fs be finite Subset of omega ; :: thesis: ( X is closed_wrt_A1-A7 & A c= X & y in Funcs fs,A implies y in X )
assume A1: ( X is closed_wrt_A1-A7 & A c= X & y in Funcs fs,A ) ; :: thesis: y in X
then consider g being Function such that
A2: ( y = g & dom g = fs & rng g c= A ) by FUNCT_2:def 2;
rng g is finite by A2, FINSET_1:26;
then [:(dom g),(rng g):] is finite by A2;
then A3: y is finite by A2, FINSET_1:13, RELAT_1:21;

now

let o be set ; :: thesis: ( o in y implies o in X )
assume A4: o in y ; :: thesis: o in X
then consider p, q being set such that
A5: o = [p,q] by A2, RELAT_1:def 1;
A6: ( p in dom g & q = g . p ) by A2, A4, A5, FUNCT_1:8;
A7: omega c= X by A1, Th7;
A8: p in omega by A2, A6;
q in rng g by A6, FUNCT_1:def 5;
then q in A by A2;
hence o in X by A1, A5, A7, A8, Th6; :: thesis: verum

end;

hence y in X by A1, A3, Th13; :: thesis: verum