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 that
A1: X is closed_wrt_A1-A7 and
A2: A c= X and
A3: y in Funcs (fs,A) ; :: thesis: y in X
consider g being Function such that
A4: y = g and
A5: dom g = fs and
A6: rng g c= A by A3, FUNCT_2:def 2;

A7: now :: thesis: for o being set st o in y holds
o in X

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

end;

rng g is finite by A5, FINSET_1:8;
then [:(dom g),(rng g):] is finite by A5;
then y is finite by A4, FINSET_1:1, RELAT_1:7;
hence y in X by A1, A7, Th13; :: thesis: verum