let n be Nat; :: thesis: for a being Integer
for i1, i2 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } is diophantine Subset of ()

let a be Integer; :: thesis: for i1, i2 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } is diophantine Subset of ()
let i1, i2 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } is diophantine Subset of ()
defpred S1[ XFinSequence of NAT ] means \$1 . i1 = a * (\$1 . i2);
defpred S2[ XFinSequence of NAT ] means 1 * (\$1 . i1) = (a * (\$1 . i2)) + 0;
A1: { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } c= { q where q is n -element XFinSequence of NAT : 1 * (q . i1) = (a * (q . i2)) + 0 }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } or y in { q where q is n -element XFinSequence of NAT : 1 * (q . i1) = (a * (q . i2)) + 0 } )
assume y in { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } ; :: thesis: y in { q where q is n -element XFinSequence of NAT : 1 * (q . i1) = (a * (q . i2)) + 0 }
then consider p being n -element XFinSequence of NAT such that
A2: ( y = p & p . i1 = a * (p . i2) ) ;
1 * (p . i1) = (a * (p . i2)) + 0 by A2;
hence y in { q where q is n -element XFinSequence of NAT : 1 * (q . i1) = (a * (q . i2)) + 0 } by A2; :: thesis: verum
end;
{ q where q is n -element XFinSequence of NAT : 1 * (q . i1) = (a * (q . i2)) + 0 } c= { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { q where q is n -element XFinSequence of NAT : 1 * (q . i1) = (a * (q . i2)) + 0 } or y in { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } )
assume y in { q where q is n -element XFinSequence of NAT : 1 * (q . i1) = (a * (q . i2)) + 0 } ; :: thesis: y in { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) }
then ex q being n -element XFinSequence of NAT st
( y = q & 1 * (q . i1) = (a * (q . i2)) + 0 ) ;
hence y in { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } ; :: thesis: verum
end;
then { q where q is n -element XFinSequence of NAT : 1 * (q . i1) = (a * (q . i2)) + 0 } = { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } by ;
hence { p where p is n -element XFinSequence of NAT : p . i1 = a * (p . i2) } is diophantine Subset of () by Th6; :: thesis: verum