let V be 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
let a, b be 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
let X be 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
let fs be finite Subset of omega; ( X is closed_wrt_A1-A7 & a in Funcs (fs,omega) & b in X implies { (a (#) x) where x is Element of V : x in b } in X )
assume that
A1:
X is closed_wrt_A1-A7
and
A2:
a in Funcs (fs,omega)
and
A3:
b in X
; { (a (#) x) where x is Element of V : x in b } in X
Funcs (fs,omega) c= X
by A1, Th8;
then A4:
{a} in X
by A1, A2, Th2;
set A = { (a (#) x) where x is Element of V : x in b } ;
set s = {a};
set B = { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } ;
A5:
{ (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } c= { (a (#) x) where x is Element of V : x in b }
{ (a (#) x) where x is Element of V : x in b } c= { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) }
then A9:
{ (a (#) x) where x is Element of V : x in b } = { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) }
by A5;
X is closed_wrt_A7
by A1;
hence
{ (a (#) x) where x is Element of V : x in b } in X
by A3, A4, A9; verum