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] & P_{2}[p] ) } ;

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

hence { p where p is F_{1}() -element XFinSequence of NAT : ( P_{1}[p] & 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: PF /\ QF c= { p where p is F

proof

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

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

then A4: ( x in PF & x in QF ) by XBOOLE_0:def 4;

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

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

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

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

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

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

then A4: ( x in PF & x in QF ) by XBOOLE_0:def 4;

then consider p being F

A5: ( x = p & P

ex p being F

( x = p & P

hence x in { p where p is F

proof

{ 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] & P_{2}[p] ) } or x in PF )

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

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

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

hence x in PF ; :: thesis: verum

end;assume x in { p where p is F

then ex p being F

( x = p & P

hence x in PF ; :: thesis: verum

proof

then
{ 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] & P_{2}[p] ) } or x in QF )

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

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

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

hence x in QF ; :: thesis: verum

end;assume x in { p where p is F

then ex p being F

( x = p & P

hence x in QF ; :: thesis: verum

hence { p where p is F