reconsider PF = { p where p is F1() -element XFinSequence of NAT : P1[p] } as diophantine Subset of (F1() -xtuples_of NAT) by A1;
reconsider QF = { p where p is F1() -element XFinSequence of NAT : P2[p] } as diophantine Subset of (F1() -xtuples_of NAT) by A2;
set PQ = { p where p is F1() -element XFinSequence of NAT : ( P1[p] & P2[p] ) } ;
A3: PF /\ QF c= { p where p is F1() -element XFinSequence of NAT : ( P1[p] & P2[p] ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PF /\ QF or x in { p where p is F1() -element XFinSequence of NAT : ( P1[p] & P2[p] ) } )
assume x in PF /\ QF ; :: thesis: x in { p where p is F1() -element XFinSequence of NAT : ( P1[p] & P2[p] ) }
then A4: ( x in PF & x in QF ) by XBOOLE_0:def 4;
then consider p being F1() -element XFinSequence of NAT such that
A5: ( x = p & P1[p] ) ;
ex p being F1() -element XFinSequence of NAT st
( x = p & P2[p] ) by A4;
hence x in { p where p is F1() -element XFinSequence of NAT : ( P1[p] & P2[p] ) } by A5; :: thesis: verum
end;
A6: { p where p is F1() -element XFinSequence of NAT : ( P1[p] & P2[p] ) } c= PF
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is F1() -element XFinSequence of NAT : ( P1[p] & P2[p] ) } or x in PF )
assume x in { p where p is F1() -element XFinSequence of NAT : ( P1[p] & P2[p] ) } ; :: thesis: x in PF
then ex p being F1() -element XFinSequence of NAT st
( x = p & P1[p] & P2[p] ) ;
hence x in PF ; :: thesis: verum
end;
{ p where p is F1() -element XFinSequence of NAT : ( P1[p] & P2[p] ) } c= QF
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is F1() -element XFinSequence of NAT : ( P1[p] & P2[p] ) } or x in QF )
assume x in { p where p is F1() -element XFinSequence of NAT : ( P1[p] & P2[p] ) } ; :: thesis: x in QF
then ex p being F1() -element XFinSequence of NAT st
( x = p & P1[p] & P2[p] ) ;
hence x in QF ; :: thesis: verum
end;
then { p where p is F1() -element XFinSequence of NAT : ( P1[p] & P2[p] ) } c= PF /\ QF by A6, XBOOLE_1:19;
hence { p where p is F1() -element XFinSequence of NAT : ( P1[p] & P2[p] ) } is diophantine Subset of (F1() -xtuples_of NAT) by A3, XBOOLE_0:def 10; :: thesis: verum