let V be Universe; :: thesis: for a, y being Element of V
for X being Subclass of V
for n being Element of omega
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & not n in fs & a in X & a c= X & y in Funcs fs,a holds
{ ({[n,x]} \/ y) where x is Element of V : x in a } in X
let a, y be Element of V; :: thesis: for X being Subclass of V
for n being Element of omega
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & not n in fs & a in X & a c= X & y in Funcs fs,a holds
{ ({[n,x]} \/ y) where x is Element of V : x in a } in X
let X be Subclass of V; :: thesis: for n being Element of omega
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & not n in fs & a in X & a c= X & y in Funcs fs,a holds
{ ({[n,x]} \/ y) where x is Element of V : x in a } in X
let n be Element of omega ; :: thesis: for fs being finite Subset of omega st X is closed_wrt_A1-A7 & not n in fs & a in X & a c= X & y in Funcs fs,a holds
{ ({[n,x]} \/ y) where x is Element of V : x in a } in X
let fs be finite Subset of omega ; :: thesis: ( X is closed_wrt_A1-A7 & not n in fs & a in X & a c= X & y in Funcs fs,a implies { ({[n,x]} \/ y) where x is Element of V : x in a } in X )
assume A1: ( X is closed_wrt_A1-A7 & not n in fs & a in X & a c= X & y in Funcs fs,a ) ; :: thesis: { ({[n,x]} \/ y) where x is Element of V : x in a } in X
then y in X by Th14;
then A2: {y} in X by A1, Th2;
set s = {y};
set Z = { ({[n,x]} \/ y) where x is Element of V : x in a } ;
set Y = { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } ;
A3: {y} c= Funcs fs,a by A1, ZFMISC_1:37;
{ ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } = { ({[n,x]} \/ y) where x is Element of V : x in a }

proof

thus { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } c= { ({[n,x]} \/ y) where x is Element of V : x in a } :: according to XBOOLE_0:def 10 :: thesis: { ({[n,x]} \/ y) where x is Element of V : x in a } c= { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) }

proof

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } or p in { ({[n,x]} \/ y) where x is Element of V : x in a } )
assume p in { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } ; :: thesis: p in { ({[n,x]} \/ y) where x is Element of V : x in a }
then consider x, z being Element of V such that
A4: ( p = {[n,x]} \/ z & x in a & z in {y} ) ;
z = y by A4, TARSKI:def 1;
hence p in { ({[n,x]} \/ y) where x is Element of V : x in a } by A4; :: thesis: verum

end;

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in { ({[n,x]} \/ y) where x is Element of V : x in a } or p in { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } )
assume p in { ({[n,x]} \/ y) where x is Element of V : x in a } ; :: thesis: p in { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) }
then A5: ex x being Element of V st
( p = {[n,x]} \/ y & x in a ) ;
y in {y} by TARSKI:def 1;
hence p in { ({[n,x]} \/ z) where x, z is Element of V : ( x in a & z in {y} ) } by A5; :: thesis: verum

end;

hence { ({[n,x]} \/ y) where x is Element of V : x in a } in X by A1, A2, A3, Th12; :: thesis: verum