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] or P2[p] ) } ;
A3: { p where p is F1() -element XFinSequence of NAT : ( P1[p] or P2[p] ) } c= PF \/ 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] or P2[p] ) } or x in PF \/ QF )
assume x in { p where p is F1() -element XFinSequence of NAT : ( P1[p] or P2[p] ) } ; :: thesis: x in PF \/ QF
then consider p being F1() -element XFinSequence of NAT such that
A4: ( x = p & ( P1[p] or P2[p] ) ) ;
( x in PF or x in QF ) by A4;
hence x in PF \/ QF by XBOOLE_0:def 3; :: thesis: verum
end;
A5: PF c= { p where p is F1() -element XFinSequence of NAT : ( P1[p] or P2[p] ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PF or x in { p where p is F1() -element XFinSequence of NAT : ( P1[p] or P2[p] ) } )
assume x in PF ; :: thesis: x in { p where p is F1() -element XFinSequence of NAT : ( P1[p] or P2[p] ) }
then ex p being F1() -element XFinSequence of NAT st
( x = p & P1[p] ) ;
hence x in { p where p is F1() -element XFinSequence of NAT : ( P1[p] or P2[p] ) } ; :: thesis: verum
end;
QF c= { p where p is F1() -element XFinSequence of NAT : ( P1[p] or P2[p] ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in QF or x in { p where p is F1() -element XFinSequence of NAT : ( P1[p] or P2[p] ) } )
assume x in QF ; :: thesis: x in { p where p is F1() -element XFinSequence of NAT : ( P1[p] or P2[p] ) }
then ex p being F1() -element XFinSequence of NAT st
( x = p & P2[p] ) ;
hence x in { p where p is F1() -element XFinSequence of NAT : ( P1[p] or P2[p] ) } ; :: thesis: verum
end;
then PF \/ QF c= { p where p is F1() -element XFinSequence of NAT : ( P1[p] or P2[p] ) } by A5, XBOOLE_1:8;
hence { p where p is F1() -element XFinSequence of NAT : ( P1[p] or P2[p] ) } is diophantine Subset of (F1() -xtuples_of NAT) by A3, XBOOLE_0:def 10; :: thesis: verum