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 S₁[ 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 : S₁[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 S₂[ 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 : S₂[p] } is diophantine Subset of ((n + 2) -xtuples_of NAT) by Th30;
defpred S₃[ XFinSequence of NAT ] means $1 . F = ($1 . X1) ! ;
A3: { p where p is n + 2 -element XFinSequence of NAT : S₃[p] } is diophantine Subset of ((n + 2) -xtuples_of NAT) by Th32;
defpred S₄[ XFinSequence of NAT ] means 1 * ($1 . X2) > (1 * ($1 . X1)) + 0;
A4: { p where p is n + 2 -element XFinSequence of NAT : S₄[p] } is diophantine Subset of ((n + 2) -xtuples_of NAT) by HILB10_3:7;
defpred S₅[ XFinSequence of NAT ] means 1 * ($1 . Y) = (1 * ($1 . F)) * ($1 . C);
A5: { p where p is n + 2 -element XFinSequence of NAT : S₅[p] } is diophantine Subset of ((n + 2) -xtuples_of NAT) by HILB10_3:9;
defpred S₆[ XFinSequence of NAT ] means ( S₂[$1] & S₃[$1] );
A6: { p where p is n + 2 -element XFinSequence of NAT : S₆[p] } is diophantine Subset of ((n + 2) -xtuples_of NAT) from HILB10_3:sch 3(A2, A3);
defpred S₇[ XFinSequence of NAT ] means ( S₆[$1] & S₄[$1] );
A7: { p where p is n + 2 -element XFinSequence of NAT : S₇[p] } is diophantine Subset of ((n + 2) -xtuples_of NAT) from HILB10_3:sch 3(A6, A4);
defpred S₈[ XFinSequence of NAT ] means ( S₇[$1] & S₅[$1] );
set PP = { p where p is n + 2 -element XFinSequence of NAT : S₈[p] } ;
A8: { p where p is n + 2 -element XFinSequence of NAT : S₈[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 : S₈[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 : S₁[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 : S₁[p] } )
assume x in PPn ; :: thesis: x in { p where p is n -element XFinSequence of NAT : S₁[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 : S₈[p] } ) ;
ex q being n + 2 -element XFinSequence of NAT st
( q = p & S₈[q] ) by A10;
then A11: S₁[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 : S₁[p] } by A11, A10; :: thesis: verum

end;

{ p where p is n -element XFinSequence of NAT : S₁[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 : S₁[p] } or x in PPn )
assume x in { p where p is n -element XFinSequence of NAT : S₁[p] } ; :: thesis: x in PPn
then consider p being n -element XFinSequence of NAT such that
A12: ( x = p & S₁[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 ;
S₈[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 : S₈[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