let V be Universe; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 A1: ( X is closed_wrt_A1-A7 & a in Funcs fs,omega & b in X ) ; :: thesis: { (a (#) x) where x is Element of V : x in b } in X
then Funcs fs,omega c= X by Th8;
then A2: {a} in X by A1, Th2;
set s = {a};
set A = { (a (#) x) where x is Element of V : x in b } ;
set B = { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } ;
A3: { (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 ) }

proof

thus { (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 ) } :: according to XBOOLE_0:def 10 :: thesis: { (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 }

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { (a (#) x) where x is Element of V : x in b } or q in { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } )
assume q in { (a (#) x) where x is Element of V : x in b } ; :: thesis: q in { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) }
then A4: ex x being Element of V st
( q = a (#) x & x in b ) ;
a in {a} by TARSKI:def 1;
hence q in { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } by A4; :: thesis: verum

end;

thus { (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 } :: thesis: verum

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } or q in { (a (#) x) where x is Element of V : x in b } )
assume q in { (y (#) x) where y, x is Element of V : ( y in {a} & x in b ) } ; :: thesis: q in { (a (#) x) where x is Element of V : x in b }
then consider y, x being Element of V such that
A5: ( q = y (#) x & y in {a} & x in b ) ;
q = a (#) x by A5, TARSKI:def 1;
hence q in { (a (#) x) where x is Element of V : x in b } by A5; :: thesis: verum

end;

end;

X is closed_wrt_A7 by A1, Def13;
hence { (a (#) x) where x is Element of V : x in b } in X by A1, A2, A3, Def12; :: thesis: verum