let n be Nat; :: thesis: for i1, i2, i3 being Element of n st n <> 0 holds
{ p where p is n -element XFinSequence of NAT : ( p . i3 = Product (((p . i2) + 1) + (- (idseq (p . i1)))) & p . i2 > p . i1 ) } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2, i3 be Element of n; :: thesis: ( n <> 0 implies { p where p is n -element XFinSequence of NAT : ( p . i3 = Product (((p . i2) + 1) + (- (idseq (p . i1)))) & p . i2 > p . i1 ) } is diophantine Subset of (n -xtuples_of NAT) )
set n2 = n + 2;
defpred S1[ XFinSequence of NAT ] means ( $1 . i3 = Product ((($1 . i2) + 1) + (- (idseq ($1 . i1)))) & $1 . i2 > $1 . i1 );
set RR = { p where p is n -element XFinSequence of NAT : S1[p] } ;
assume A1: n <> 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : ( p . i3 = Product (((p . i2) + 1) + (- (idseq (p . i1)))) & p . i2 > p . i1 ) } is diophantine Subset of (n -xtuples_of NAT)
n = n + 0 ;
then reconsider Y = i3, X2 = i2, X1 = i1, C = n, F = n + 1 as Element of n + 2 by HILB10_3:2, HILB10_3:3;
defpred S2[ XFinSequence of NAT ] means ( $1 . X2 >= $1 . X1 & $1 . C = ($1 . X2) choose ($1 . X1) );
A2: { p where p is n + 2 -element XFinSequence of NAT : S2[p] } is diophantine Subset of ((n + 2) -xtuples_of NAT) by Th30;
defpred S3[ XFinSequence of NAT ] means $1 . F = ($1 . X1) ! ;
A3: { p where p is n + 2 -element XFinSequence of NAT : S3[p] } is diophantine Subset of ((n + 2) -xtuples_of NAT) by Th32;
defpred S4[ XFinSequence of NAT ] means 1 * ($1 . X2) > (1 * ($1 . X1)) + 0;
A4: { p where p is n + 2 -element XFinSequence of NAT : S4[p] } is diophantine Subset of ((n + 2) -xtuples_of NAT) by HILB10_3:7;
defpred S5[ XFinSequence of NAT ] means 1 * ($1 . Y) = (1 * ($1 . F)) * ($1 . C);
A5: { p where p is n + 2 -element XFinSequence of NAT : S5[p] } is diophantine Subset of ((n + 2) -xtuples_of NAT) by HILB10_3:9;
defpred S6[ XFinSequence of NAT ] means ( S2[$1] & S3[$1] );
A6: { p where p is n + 2 -element XFinSequence of NAT : S6[p] } is diophantine Subset of ((n + 2) -xtuples_of NAT) from HILB10_3:sch 3(A2, A3);
 defpred S7[ XFinSequence of NAT ] means ( S6[$1] & S4[$1] );
A7: { p where p is n + 2 -element XFinSequence of NAT : S7[p] } is diophantine Subset of ((n + 2) -xtuples_of NAT) from HILB10_3:sch 3(A6, A4);
 defpred S8[ XFinSequence of NAT ] means ( S7[$1] & S5[$1] );
set PP = { p where p is n + 2 -element XFinSequence of NAT : S8[p] } ;
A8: { p where p is n + 2 -element XFinSequence of NAT : S8[p] } is diophantine Subset of ((n + 2) -xtuples_of NAT) from HILB10_3:sch 3(A7, A5);
 reconsider PPn = { (p | n) where p is n + 2 -element XFinSequence of NAT : p in { p where p is n + 2 -element XFinSequence of NAT : S8[p] } } as diophantine Subset of (n -xtuples_of NAT) by NAT_1:11, HILB10_3:5, A8;
A9: PPn c= { p where p is n -element XFinSequence of NAT : S1[p] }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PPn or x in { p where p is n -element XFinSequence of NAT : S1[p] } )
assume x in PPn ; :: thesis: x in { p where p is n -element XFinSequence of NAT : S1[p] }
then consider p being n + 2 -element XFinSequence of NAT such that
A10: ( x = p | n & p in { p where p is n + 2 -element XFinSequence of NAT : S8[p] } ) ;
ex q being n + 2 -element XFinSequence of NAT st
( q = p & S8[q] ) by A10;
then A11: S1[p] by Th23;
( (p | n) . X2 = p . i2 & (p | n) . X1 = p . i1 & (p | n) . Y = p . i3 ) by A1, HILB10_3:4;
hence x in { p where p is n -element XFinSequence of NAT : S1[p] } by A11, A10; :: thesis: verum
end;
{ p where p is n -element XFinSequence of NAT : S1[p] } c= PPn
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is n -element XFinSequence of NAT : S1[p] } or x in PPn )
assume x in { p where p is n -element XFinSequence of NAT : S1[p] } ; :: thesis: x in PPn
then consider p being n -element XFinSequence of NAT such that
A12: ( x = p & S1[p] ) ;
reconsider F = (p . i1) ! , C = (p . i2) choose (p . i1) as Element of NAT ;
set Y = <%C,F%>;
set PY = p ^ <%C,F%>;
A13: ( len p = n & len <%C,F%> = 2 ) by CARD_1:def 7;
A14: (p ^ <%C,F%>) | n = p by A13, AFINSQ_1:57;
A15: (p ^ <%C,F%>) . i2 = ((p ^ <%C,F%>) | n) . i2 by A1, HILB10_3:4
.= p . i2 by A13, AFINSQ_1:57 ;
A16: (p ^ <%C,F%>) . i3 = ((p ^ <%C,F%>) | n) . i3 by A1, HILB10_3:4
.= p . i3 by A13, AFINSQ_1:57 ;
0 in dom <%C,F%> by AFINSQ_1:66;
then A17: (p ^ <%C,F%>) . (n + 0) = <%C,F%> . 0 by A13, AFINSQ_1:def 3
.= C ;
1 in dom <%C,F%> by A13, AFINSQ_1:66;
then A18: (p ^ <%C,F%>) . (n + 1) = <%C,F%> . 1 by A13, AFINSQ_1:def 3
.= F ;
S8[p ^ <%C,F%>] by A12, A14, A1, HILB10_3:4, A16, A15, A17, A18, Th23;
then p ^ <%C,F%> in { p where p is n + 2 -element XFinSequence of NAT : S8[p] } ;
hence x in PPn by A14, A12; :: thesis: verum
end;
hence { p where p is n -element XFinSequence of NAT : ( p . i3 = Product (((p . i2) + 1) + (- (idseq (p . i1)))) & p . i2 > p . i1 ) } is diophantine Subset of (n -xtuples_of NAT) by A9, XBOOLE_0:def 10; :: thesis: verum