reconsider PF = { p where p is F_{1}() -element XFinSequence of NAT : P_{1}[p] } as diophantine Subset of (F_{1}() -xtuples_of NAT) by A1;

reconsider QF = { p where p is F_{1}() -element XFinSequence of NAT : P_{2}[p] } as diophantine Subset of (F_{1}() -xtuples_of NAT) by A2;

set PQ = { p where p is F_{1}() -element XFinSequence of NAT : ( P_{1}[p] or P_{2}[p] ) } ;

A3: { p where p is F_{1}() -element XFinSequence of NAT : ( P_{1}[p] or P_{2}[p] ) } c= PF \/ QF
_{1}() -element XFinSequence of NAT : ( P_{1}[p] or P_{2}[p] ) }
_{1}() -element XFinSequence of NAT : ( P_{1}[p] or P_{2}[p] ) }
_{1}() -element XFinSequence of NAT : ( P_{1}[p] or P_{2}[p] ) }
by A5, XBOOLE_1:8;

hence { p where p is F_{1}() -element XFinSequence of NAT : ( P_{1}[p] or P_{2}[p] ) } is diophantine Subset of (F_{1}() -xtuples_of NAT)
by A3, XBOOLE_0:def 10; :: thesis: verum

reconsider QF = { p where p is F

set PQ = { p where p is F

A3: { p where p is F

proof

A5:
PF c= { p where p is F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is F_{1}() -element XFinSequence of NAT : ( P_{1}[p] or P_{2}[p] ) } or x in PF \/ QF )

assume x in { p where p is F_{1}() -element XFinSequence of NAT : ( P_{1}[p] or P_{2}[p] ) }
; :: thesis: x in PF \/ QF

then consider p being F_{1}() -element XFinSequence of NAT such that

A4: ( x = p & ( P_{1}[p] or P_{2}[p] ) )
;

( x in PF or x in QF ) by A4;

hence x in PF \/ QF by XBOOLE_0:def 3; :: thesis: verum

end;assume x in { p where p is F

then consider p being F

A4: ( x = p & ( P

( x in PF or x in QF ) by A4;

hence x in PF \/ QF by XBOOLE_0:def 3; :: thesis: verum

proof

QF c= { p where p is F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PF or x in { p where p is F_{1}() -element XFinSequence of NAT : ( P_{1}[p] or P_{2}[p] ) } )

assume x in PF ; :: thesis: x in { p where p is F_{1}() -element XFinSequence of NAT : ( P_{1}[p] or P_{2}[p] ) }

then ex p being F_{1}() -element XFinSequence of NAT st

( x = p & P_{1}[p] )
;

hence x in { p where p is F_{1}() -element XFinSequence of NAT : ( P_{1}[p] or P_{2}[p] ) }
; :: thesis: verum

end;assume x in PF ; :: thesis: x in { p where p is F

then ex p being F

( x = p & P

hence x in { p where p is F

proof

then
PF \/ QF c= { p where p is F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in QF or x in { p where p is F_{1}() -element XFinSequence of NAT : ( P_{1}[p] or P_{2}[p] ) } )

assume x in QF ; :: thesis: x in { p where p is F_{1}() -element XFinSequence of NAT : ( P_{1}[p] or P_{2}[p] ) }

then ex p being F_{1}() -element XFinSequence of NAT st

( x = p & P_{2}[p] )
;

hence x in { p where p is F_{1}() -element XFinSequence of NAT : ( P_{1}[p] or P_{2}[p] ) }
; :: thesis: verum

end;assume x in QF ; :: thesis: x in { p where p is F

then ex p being F

( x = p & P

hence x in { p where p is F

hence { p where p is F