let V be Universe; :: thesis: for a, b 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 & b in X & b c= Funcs fs,a holds
{ ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X
let a, b 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 & b in X & b c= Funcs fs,a holds
{ ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } 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 & b in X & b c= Funcs fs,a holds
{ ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } 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 & b in X & b c= Funcs fs,a holds
{ ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X
let fs be finite Subset of omega ; :: thesis: ( X is closed_wrt_A1-A7 & not n in fs & a in X & b in X & b c= Funcs fs,a implies { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X )
assume A1: ( X is closed_wrt_A1-A7 & not n in fs & a in X & b in X & b c= Funcs fs,a ) ; :: thesis: { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X
set Z = { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } ;
A2: Funcs {n},a in X by A1, Th9;
then reconsider F = Funcs {n},a as Element of V ;
set Y = { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } ;
A3: X is closed_wrt_A5 by A1, Def13;
{ (x \/ y) where x, y is Element of V : ( x in F & y in b ) } = { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) }

proof

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

proof

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } or p in { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } )
assume p in { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } ; :: thesis: p in { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) }
then consider x, y being Element of V such that
A4: ( p = x \/ y & x in F & y in b ) ;
consider g being Function such that
A5: ( x = g & dom g = {n} & rng g c= a ) by A4, FUNCT_2:def 2;
n in dom g by A5, TARSKI:def 1;
then A6: g . n in rng g by FUNCT_1:def 5;
then reconsider z = g . n as Element of V by A1, A5, Th1;
p = {[n,z]} \/ y by A4, A5, GRFUNC_1:18;
hence p in { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } by A4, A5, A6; :: thesis: verum

end;

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } or p in { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } )
assume p in { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } ; :: thesis: p in { (x \/ y) where x, y is Element of V : ( x in F & y in b ) }
then consider x, y being Element of V such that
A7: ( p = {[n,x]} \/ y & x in a & y in b ) ;
reconsider g = {[n,x]} as Function by GRFUNC_1:15;
A8: dom g = {n} by RELAT_1:23;
rng g = {x} by RELAT_1:23;
then rng g c= a by A7, ZFMISC_1:37;
then A9: {[n,x]} in F by A8, FUNCT_2:def 2;
then reconsider z = {[n,x]} as Element of V by A2, Th1;
p = z \/ y by A7;
hence p in { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } by A7, A9; :: thesis: verum

end;

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