let V be Universe; :: thesis: for a, b being Element of V
for X being Subclass of V
for n being Element of omega st X is closed_wrt_A1-A7 & a in X & b in X 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 st X is closed_wrt_A1-A7 & a in X & b in X 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 st X is closed_wrt_A1-A7 & a in X & b in X 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: ( X is closed_wrt_A1-A7 & a in X & b in X implies { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X )
assume that
A1: X is closed_wrt_A1-A7 and
A2: a in X and
A3: b in X ; :: thesis: { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X
A4: Funcs ({n},a) in X by A1, A2, Th9;
then reconsider F = Funcs ({n},a) as Element of V ;
set Z = { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } ;
set Y = { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } ;
A5: { (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 object ; :: 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
A6: p = x \/ y and
A7: x in F and
A8: y in b ;
consider g being Function such that
A9: x = g and
A10: dom g = {n} and
A11: rng g c= a by A7, FUNCT_2:def 2;
n in dom g by A10, TARSKI:def 1;
then A12: g . n in rng g by FUNCT_1:def 3;
then reconsider z = g . n as Element of V by A2, A11, Th1;
p = {[n,z]} \/ y by A6, A9, A10, GRFUNC_1:7;
hence p in { ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } by A8, A11, A12; :: thesis: verum

end;

let p be object ; :: 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
A13: p = {[n,x]} \/ y and
A14: x in a and
A15: y in b ;
reconsider g = {[n,x]} as Function ;
rng g = {x} by RELAT_1:9;
then ( dom g = {n} & rng g c= a ) by A14, RELAT_1:9, ZFMISC_1:31;
then A16: {[n,x]} in F by FUNCT_2:def 2;
then reconsider z = {[n,x]} as Element of V by A4, Th1;
p = z \/ y by A13;
hence p in { (x \/ y) where x, y is Element of V : ( x in F & y in b ) } by A15, A16; :: thesis: verum

end;

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