let n be Nat; :: thesis: for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } is diophantine Subset of ()
let i1, i2, i3 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } is diophantine Subset of ()
set n9 = n + 9;
set WW = { p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } ;
{ p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } c= n -xtuples_of NAT
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 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } or y in n -xtuples_of NAT )
assume y in { p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } ; :: thesis:
then ex p being n -element XFinSequence of NAT st
( y = p & p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) ;
hence y in n -xtuples_of NAT by HILB10_2:def 5; :: thesis: verum
end;
then reconsider WW = { p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } as Subset of () ;
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } is diophantine Subset of ()
then WW is diophantine Subset of () ;
hence { p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } is diophantine Subset of () ; :: thesis: verum
end;
suppose A1: n <> 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } is diophantine Subset of ()
n = n + 0 ;
then reconsider N = n, I1 = i1, I2 = i2, I3 = i3, N1 = n + 1, N2 = n + 2, N3 = n + 3, N4 = n + 4, N5 = n + 5, N6 = n + 6, N7 = n + 7, N8 = n + 8 as Element of n + 9 by ;
defpred S1[ XFinSequence of NAT ] means 1 * (\$1 . I2) > (0 * (\$1 . I1)) + 1;
A2: { p where p is n + 9 -element XFinSequence of NAT : S1[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) by Th7;
defpred S2[ XFinSequence of NAT ] means [(1 * (\$1 . N)),(1 * (\$1 . I1))] is Pell's_solution of ((1 * (\$1 . I2)) ^2) -' 1;
A3: { p where p is n + 9 -element XFinSequence of NAT : S2[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) by Th22;
defpred S3[ XFinSequence of NAT ] means [(1 * (\$1 . N1)),(1 * (\$1 . N2))] is Pell's_solution of ((1 * (\$1 . I2)) ^2) -' 1;
A4: { p where p is n + 9 -element XFinSequence of NAT : S3[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) by Th22;
defpred S4[ XFinSequence of NAT ] means 1 * (\$1 . N2) >= (1 * (\$1 . I1)) + 0;
A5: { p where p is n + 9 -element XFinSequence of NAT : S4[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) by Th8;
defpred S5[ XFinSequence of NAT ] means 1 * (\$1 . N3) > (1 * (\$1 . I1)) + 0;
A6: { p where p is n + 9 -element XFinSequence of NAT : S5[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) by Th7;
defpred S6[ XFinSequence of NAT ] means 1 * (\$1 . I1) >= (1 * (\$1 . I3)) + 0;
A7: { p where p is n + 9 -element XFinSequence of NAT : S6[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) by Th8;
defpred S7[ XFinSequence of NAT ] means [(1 * (\$1 . N4)),(1 * (\$1 . N5))] is Pell's_solution of ((1 * (\$1 . N3)) ^2) -' 1;
A8: { p where p is n + 9 -element XFinSequence of NAT : S7[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) by Th22;
defpred S8[ XFinSequence of NAT ] means 1 * (\$1 . N5),1 * (\$1 . I1) are_congruent_mod 1 * (\$1 . N1);
A9: { p where p is n + 9 -element XFinSequence of NAT : S8[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) by Th21;
defpred S9[ XFinSequence of NAT ] means 1 * (\$1 . N3),1 * (\$1 . I2) are_congruent_mod 1 * (\$1 . N1);
A10: { p where p is n + 9 -element XFinSequence of NAT : S9[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) by Th21;
defpred S10[ XFinSequence of NAT ] means 1 * (\$1 . N5),1 * (\$1 . I3) are_congruent_mod 1 * (\$1 . N6);
A11: { p where p is n + 9 -element XFinSequence of NAT : S10[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) by Th21;
defpred S11[ XFinSequence of NAT ] means 1 * (\$1 . N3),1 * (\$1 . N8) are_congruent_mod 1 * (\$1 . N6);
A12: { p where p is n + 9 -element XFinSequence of NAT : S11[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) by Th21;
defpred S12[ XFinSequence of NAT ] means 1 * (\$1 . N2),0 * (\$1 . N3) are_congruent_mod 1 * (\$1 . N7);
A13: { p where p is n + 9 -element XFinSequence of NAT : S12[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) by Th21;
defpred S13[ XFinSequence of NAT ] means 1 = \$1 . N8;
A14: { p where p is n + 9 -element XFinSequence of NAT : S13[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) by Th14;
defpred S14[ XFinSequence of NAT ] means 2 * (\$1 . I1) = \$1 . N6;
A15: { p where p is n + 9 -element XFinSequence of NAT : S14[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) by Th12;
defpred S15[ XFinSequence of NAT ] means (1 * (\$1 . I1)) * (\$1 . I1) = 1 * (\$1 . N7);
A16: { p where p is n + 9 -element XFinSequence of NAT : S15[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) by Th9;
defpred S16[ XFinSequence of NAT ] means ( S1[\$1] & S2[\$1] );
defpred S17[ XFinSequence of NAT ] means ( S3[\$1] & S4[\$1] );
defpred S18[ XFinSequence of NAT ] means ( S5[\$1] & S6[\$1] );
defpred S19[ XFinSequence of NAT ] means ( S7[\$1] & S8[\$1] );
defpred S20[ XFinSequence of NAT ] means ( S9[\$1] & S10[\$1] );
defpred S21[ XFinSequence of NAT ] means ( S11[\$1] & S12[\$1] );
defpred S22[ XFinSequence of NAT ] means ( S13[\$1] & S14[\$1] );
{ p where p is n + 9 -element XFinSequence of NAT : ( S1[p] & S2[p] ) } is diophantine Subset of ((n + 9) -xtuples_of NAT) from then A17: { p where p is n + 9 -element XFinSequence of NAT : S16[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) ;
{ p where p is n + 9 -element XFinSequence of NAT : ( S3[p] & S4[p] ) } is diophantine Subset of ((n + 9) -xtuples_of NAT) from then A18: { p where p is n + 9 -element XFinSequence of NAT : S17[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) ;
{ p where p is n + 9 -element XFinSequence of NAT : ( S5[p] & S6[p] ) } is diophantine Subset of ((n + 9) -xtuples_of NAT) from then A19: { p where p is n + 9 -element XFinSequence of NAT : S18[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) ;
{ p where p is n + 9 -element XFinSequence of NAT : ( S7[p] & S8[p] ) } is diophantine Subset of ((n + 9) -xtuples_of NAT) from then A20: { p where p is n + 9 -element XFinSequence of NAT : S19[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) ;
{ p where p is n + 9 -element XFinSequence of NAT : ( S9[p] & S10[p] ) } is diophantine Subset of ((n + 9) -xtuples_of NAT) from then A21: { p where p is n + 9 -element XFinSequence of NAT : S20[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) ;
{ p where p is n + 9 -element XFinSequence of NAT : ( S11[p] & S12[p] ) } is diophantine Subset of ((n + 9) -xtuples_of NAT) from then A22: { p where p is n + 9 -element XFinSequence of NAT : S21[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) ;
{ p where p is n + 9 -element XFinSequence of NAT : ( S13[p] & S14[p] ) } is diophantine Subset of ((n + 9) -xtuples_of NAT) from then A23: { p where p is n + 9 -element XFinSequence of NAT : S22[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) ;
defpred S23[ XFinSequence of NAT ] means ( S16[\$1] & S17[\$1] );
defpred S24[ XFinSequence of NAT ] means ( S18[\$1] & S19[\$1] );
defpred S25[ XFinSequence of NAT ] means ( S20[\$1] & S21[\$1] );
defpred S26[ XFinSequence of NAT ] means ( S22[\$1] & S15[\$1] );
{ p where p is n + 9 -element XFinSequence of NAT : ( S16[p] & S17[p] ) } is diophantine Subset of ((n + 9) -xtuples_of NAT) from then A24: { p where p is n + 9 -element XFinSequence of NAT : S23[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) ;
{ p where p is n + 9 -element XFinSequence of NAT : ( S18[p] & S19[p] ) } is diophantine Subset of ((n + 9) -xtuples_of NAT) from then A25: { p where p is n + 9 -element XFinSequence of NAT : S24[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) ;
{ p where p is n + 9 -element XFinSequence of NAT : ( S20[p] & S21[p] ) } is diophantine Subset of ((n + 9) -xtuples_of NAT) from then A26: { p where p is n + 9 -element XFinSequence of NAT : S25[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) ;
{ p where p is n + 9 -element XFinSequence of NAT : ( S22[p] & S15[p] ) } is diophantine Subset of ((n + 9) -xtuples_of NAT) from then A27: { p where p is n + 9 -element XFinSequence of NAT : S26[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) ;
defpred S27[ XFinSequence of NAT ] means ( S23[\$1] & S24[\$1] );
defpred S28[ XFinSequence of NAT ] means ( S25[\$1] & S26[\$1] );
{ p where p is n + 9 -element XFinSequence of NAT : ( S23[p] & S24[p] ) } is diophantine Subset of ((n + 9) -xtuples_of NAT) from then A28: { p where p is n + 9 -element XFinSequence of NAT : S27[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) ;
{ p where p is n + 9 -element XFinSequence of NAT : ( S25[p] & S26[p] ) } is diophantine Subset of ((n + 9) -xtuples_of NAT) from then A29: { p where p is n + 9 -element XFinSequence of NAT : S28[p] } is diophantine Subset of ((n + 9) -xtuples_of NAT) ;
defpred S29[ XFinSequence of NAT ] means ( S27[\$1] & S28[\$1] );
A30: { p where p is n + 9 -element XFinSequence of NAT : ( S27[p] & S28[p] ) } is diophantine Subset of ((n + 9) -xtuples_of NAT) from set DD = { p where p is n + 9 -element XFinSequence of NAT : S29[p] } ;
set DDR = { (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } } ;
A31: { (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } } is diophantine Subset of () by ;
A32: { (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } } c= WW
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in { (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } } or o in WW )
assume A33: o in { (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } } ; :: thesis: o in WW
consider p being n + 9 -element XFinSequence of NAT such that
A34: ( o = p | n & p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } ) by A33;
consider q being n + 9 -element XFinSequence of NAT such that
A35: ( p = q & S29[q] ) by A34;
( len p = n + 9 & n + 9 >= n ) by ;
then len (p | n) = n by AFINSQ_1:54;
then reconsider pn = p | n as n -element XFinSequence of NAT by CARD_1:def 7;
A36: ( pn . I3 = p . i3 & pn . I2 = p . i2 & (p | n) . I1 = p . i1 ) by ;
( 1 * (p . I2) > (0 * (p . I1)) + 1 & [(1 * (p . N)),(1 * (p . I1))] is Pell's_solution of ((1 * (p . I2)) ^2) -' 1 & [(1 * (p . N1)),(1 * (p . N2))] is Pell's_solution of ((1 * (p . I2)) ^2) -' 1 & 1 * (p . N2) >= (1 * (p . I1)) + 0 & 1 * (p . N3) > (1 * (p . I1)) + 0 & 1 * (p . I1) >= (1 * (p . I3)) + 0 & [(1 * (p . N4)),(1 * (p . N5))] is Pell's_solution of ((1 * (p . N3)) ^2) -' 1 & 1 * (p . N5),1 * (p . I1) are_congruent_mod 1 * (p . N1) & 1 * (p . N3),1 * (p . I2) are_congruent_mod 1 * (p . N1) & 1 * (p . N5),1 * (p . I3) are_congruent_mod 1 * (2 * (p . I1)) & 1 * (p . N3),1 * 1 are_congruent_mod 1 * (2 * (p . I1)) & 1 * (p . N2),0 * (p . N3) are_congruent_mod (p . I1) ^2 ) by ;
then ( pn . i1 = Py ((pn . i2),(pn . i3)) & pn . i2 > 1 ) by ;
hence o in WW by A34; :: thesis: verum
end;
WW c= { (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } }
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in WW or o in { (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } } )
assume A37: o in WW ; :: thesis: o in { (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } }
consider p being n -element XFinSequence of NAT such that
A38: ( o = p & p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) by A37;
set y = p . i1;
set a = p . i2;
set z = p . i3;
consider x, x1, y1, A, x2, y2 being Nat such that
A39: ( p . i2 > 1 & [x,(p . i1)] is Pell's_solution of ((p . i2) ^2) -' 1 & [x1,y1] is Pell's_solution of ((p . i2) ^2) -' 1 & y1 >= p . i1 & A > p . i1 & p . i1 >= p . i3 & [x2,y2] is Pell's_solution of (A ^2) -' 1 & y2,p . i1 are_congruent_mod x1 & A,p . i2 are_congruent_mod x1 & y2,p . i3 are_congruent_mod 2 * (p . i1) & A,1 are_congruent_mod 2 * (p . i1) & y1, 0 are_congruent_mod (p . i1) ^2 ) by ;
reconsider x = x, x1 = x1, y1 = y1, A = A, x2 = x2, y2 = y2 as Element of NAT by ORDINAL1:def 12;
reconsider 2y = 2 * (p . i1) as Element of NAT ;
reconsider yy = (p . i1) * (p . i1) as Element of NAT ;
reconsider Z = 1 as Element of NAT ;
set Y = (((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>;
set PY = p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>);
A40: ( len p = n & len ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) = 9 ) by CARD_1:def 7;
A41: (p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) | n = p by ;
0 in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) by ;
then A42: (p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 0) = ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 0 by
.= x by AFINSQ_1:50 ;
1 in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) by ;
then A43: (p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 1) = ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 1 by
.= x1 by AFINSQ_1:50 ;
2 in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) by ;
then A44: (p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 2) = ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 2 by
.= y1 by AFINSQ_1:50 ;
3 in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) by ;
then A45: (p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 3) = ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 3 by
.= A by AFINSQ_1:50 ;
4 in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) by ;
then A46: (p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 4) = ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 4 by
.= x2 by AFINSQ_1:50 ;
5 in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) by ;
then A47: (p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 5) = ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 5 by
.= y2 by AFINSQ_1:50 ;
6 in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) by ;
then (p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 6) = ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 6 by
.= 2y by AFINSQ_1:50 ;
then A48: ( (p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . N6 = 2 * (p . i1) & 2 * (p . i1) = 2 * ((p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . I1) ) by A41, A1, Th4;
7 in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) by ;
then A49: (p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 7) = ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 7 by
.= yy by AFINSQ_1:50 ;
8 in dom ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) by ;
then A50: (p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)) . (n + 8) = ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) . 8 by
.= Z by AFINSQ_1:50 ;
S29[p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>)] by SQUARE_1:def 1, A39, A42, A45, A46, A47, A1, Th4, A43, A41, A50, A48, A49, A44;
then p ^ ((((((((<%x%> ^ <%x1%>) ^ <%y1%>) ^ <%A%>) ^ <%x2%>) ^ <%y2%>) ^ <%2y%>) ^ <%yy%>) ^ <%Z%>) in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } ;
hence o in { (p | n) where p is n + 9 -element XFinSequence of NAT : p in { p where p is n + 9 -element XFinSequence of NAT : S29[p] } } by ; :: thesis: verum
end;
hence { p where p is n -element XFinSequence of NAT : ( p . i1 = Py ((p . i2),(p . i3)) & p . i2 > 1 ) } is diophantine Subset of () by ; :: thesis: verum
end;
end;