let i, n1, n2 be Nat; :: thesis: for n being Nat
for i1 being Element of n holds { p where p is b1 -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | n2)) } is diophantine Subset of (n -xtuples_of NAT)
defpred S1[ Nat] means for n being Nat st $1 + n1 <= n holds
for i1 being Element of n holds { p where p is b1 -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | $1)) } is diophantine Subset of (n -xtuples_of NAT);
A1: S1[ 0 ]
proof
let n be Nat; :: thesis: ( 0 + n1 <= n implies for i1 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | 0)) } is diophantine Subset of (n -xtuples_of NAT) )
assume 0 + n1 <= n ; :: thesis: for i1 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | 0)) } is diophantine Subset of (n -xtuples_of NAT)
let i1 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | 0)) } is diophantine Subset of (n -xtuples_of NAT)
defpred S2[ XFinSequence of NAT ] means $1 . i1 = Product (i + (($1 /^ n1) | 0));
defpred S3[ XFinSequence of NAT ] means $1 . i1 = 1;
A2: for p being n -element XFinSequence of NAT holds
( S2[p] iff S3[p] ) by Th4;
{ p where p is n -element XFinSequence of NAT : S2[p] } = { q where q is n -element XFinSequence of NAT : S3[q] } from HILB10_3:sch 2(A2);
 hence { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | 0)) } is diophantine Subset of (n -xtuples_of NAT) by HILB10_3:14; :: thesis: verum
end;
A3: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A4: S1[m] ; :: thesis: S1[m + 1]
let n be Nat; :: thesis: ( (m + 1) + n1 <= n implies for i1 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | (m + 1))) } is diophantine Subset of (n -xtuples_of NAT) )
assume A5: (m + 1) + n1 <= n ; :: thesis: for i1 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | (m + 1))) } is diophantine Subset of (n -xtuples_of NAT)
set m1 = m + 1;
set X = n + 1;
let i1 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | (m + 1))) } is diophantine Subset of (n -xtuples_of NAT)
m < m + 1 by NAT_1:13;
then n1 + m < n1 + (m + 1) by XREAL_1:8;
then A6: n1 + m < n by A5, XXREAL_0:2;
then n1 + m in Segm n by NAT_1:44;
then reconsider n1m = n1 + m as Element of n ;
A7: n < n + 1 by NAT_1:13;
then n in Segm (n + 1) by NAT_1:44;
then reconsider N = n, I1 = i1, N1M = n1m as Element of n + 1 by HILB10_3:2;
defpred S2[ XFinSequence of NAT ] means $1 . N = Product (i + (($1 /^ n1) | m));
defpred S3[ XFinSequence of NAT ] means $1 . I1 = ((1 * ($1 . N1M)) + i) * ($1 . N);
n1 + m <= n + 1 by A6, NAT_1:13;
then A8: { p where p is n + 1 -element XFinSequence of NAT : S2[p] } is diophantine Subset of ((n + 1) -xtuples_of NAT) by A4;
A9: { p where p is n + 1 -element XFinSequence of NAT : S3[p] } is diophantine Subset of ((n + 1) -xtuples_of NAT) by Th25;
set PQ = { p where p is n + 1 -element XFinSequence of NAT : ( S2[p] & S3[p] ) } ;
A10: { p where p is n + 1 -element XFinSequence of NAT : ( S2[p] & S3[p] ) } is diophantine Subset of ((n + 1) -xtuples_of NAT) from HILB10_3:sch 3(A8, A9);
 set PQr = { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S2[p] & S3[p] ) } } ;
set S = { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | (m + 1))) } ;
A11: { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S2[p] & S3[p] ) } } is diophantine Subset of (n -xtuples_of NAT) by HILB10_3:5, A7, A10;
A12: ( n1 <= n1 + (m + 1) & n1 + (m + 1) <= n ) by A5, NAT_1:11;
then A13: n -' n1 = n - n1 by XXREAL_0:2, XREAL_1:233;
A14: m + 1 <= n - n1 by A5, XREAL_1:19;
m < m + 1 by NAT_1:13;
then A15: ( Segm m c= Segm (m + 1) & m in Segm (m + 1) ) by NAT_1:39, NAT_1:44;
A16: { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | (m + 1))) } c= { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S2[p] & S3[p] ) } }
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 = Product (i + ((p /^ n1) | (m + 1))) } or y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S2[p] & S3[p] ) } } )
assume y in { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | (m + 1))) } ; :: thesis: y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S2[p] & S3[p] ) } }
then consider p being n -element XFinSequence of NAT such that
A17: ( y = p & p . i1 = Product (i + ((p /^ n1) | (m + 1))) ) ;
A18: len p = n by CARD_1:def 7;
then A19: len (p /^ n1) >= m + 1 by A14, A13, AFINSQ_2:def 2;
then len ((p /^ n1) | (m + 1)) = m + 1 by AFINSQ_1:54;
then A20: (p /^ n1) | (m + 1) = (((p /^ n1) | (m + 1)) | m) ^ <%(((p /^ n1) | (m + 1)) . m)%> by AFINSQ_1:56;
( ((p /^ n1) | (m + 1)) | m = (p /^ n1) | m & ((p /^ n1) | (m + 1)) . m = (p /^ n1) . m & m in dom (p /^ n1) ) by A19, AFINSQ_1:53, RELAT_1:74, A15;
then (p /^ n1) | (m + 1) = ((p /^ n1) | m) ^ <%(p . n1m)%> by A20, AFINSQ_2:def 2;
then i + ((p /^ n1) | (m + 1)) = (i + ((p /^ n1) | m)) ^ (i + <%(p . n1m)%>) by Th8
.= (i + ((p /^ n1) | m)) ^ <%(i + (p . n1m))%> by Th9 ;
then A21: Product (i + ((p /^ n1) | (m + 1))) = (Product (i + ((p /^ n1) | m))) * (Product <%(i + (p . n1m))%>) by Th7
.= (Product (i + ((p /^ n1) | m))) * (i + (p . n1m)) by Th5 ;
reconsider P = Product (i + ((p /^ n1) | m)) as Element of NAT by ORDINAL1:def 12;
reconsider pP = p ^ <%P%> as n + 1 -element XFinSequence of NAT ;
A22: len (p /^ n1) > m by A19, NAT_1:13;
A23: (pP /^ n1) | m = ((p /^ n1) ^ <%P%>) | m by Th10, A18, A12, XXREAL_0:2
.= (p /^ n1) | m by AFINSQ_1:58, A22 ;
A24: pP | n = p by A18, AFINSQ_1:57;
A25: ( pP . I1 = p . i1 & pP . N1M = p . n1m ) by A5, A24, HILB10_3:4;
( S2[pP] & S3[pP] ) by A23, A25, A21, A18, AFINSQ_1:36, A17;
then pP in { p where p is n + 1 -element XFinSequence of NAT : ( S2[p] & S3[p] ) } ;
hence y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S2[p] & S3[p] ) } } by A17, A24; :: thesis: verum
end;
{ (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S2[p] & S3[p] ) } } c= { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | (m + 1))) }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S2[p] & S3[p] ) } } or y in { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | (m + 1))) } )
assume y in { (p | n) where p is n + 1 -element XFinSequence of NAT : p in { p where p is n + 1 -element XFinSequence of NAT : ( S2[p] & S3[p] ) } } ; :: thesis: y in { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | (m + 1))) }
then consider pP being n + 1 -element XFinSequence of NAT such that
A26: ( y = pP | n & pP in { p where p is n + 1 -element XFinSequence of NAT : ( S2[p] & S3[p] ) } ) ;
A27: ex q being n + 1 -element XFinSequence of NAT st
( pP = q & S2[q] & S3[q] ) by A26;
A28: len pP = n + 1 by CARD_1:def 7;
A29: len (pP | n) = n by CARD_1:def 7;
set p = pP | n;
A30: len ((pP | n) /^ n1) >= m + 1 by A14, A13, A29, AFINSQ_2:def 2;
then len (((pP | n) /^ n1) | (m + 1)) = m + 1 by AFINSQ_1:54;
then A31: ((pP | n) /^ n1) | (m + 1) = ((((pP | n) /^ n1) | (m + 1)) | m) ^ <%((((pP | n) /^ n1) | (m + 1)) . m)%> by AFINSQ_1:56;
( (((pP | n) /^ n1) | (m + 1)) | m = ((pP | n) /^ n1) | m & (((pP | n) /^ n1) | (m + 1)) . m = ((pP | n) /^ n1) . m & m in dom ((pP | n) /^ n1) ) by A30, AFINSQ_1:53, RELAT_1:74, A15;
then ((pP | n) /^ n1) | (m + 1) = (((pP | n) /^ n1) | m) ^ <%((pP | n) . n1m)%> by A31, AFINSQ_2:def 2;
then i + (((pP | n) /^ n1) | (m + 1)) = (i + (((pP | n) /^ n1) | m)) ^ (i + <%((pP | n) . n1m)%>) by Th8
.= (i + (((pP | n) /^ n1) | m)) ^ <%(i + ((pP | n) . n1m))%> by Th9 ;
then A32: Product (i + (((pP | n) /^ n1) | (m + 1))) = (Product (i + (((pP | n) /^ n1) | m))) * (Product <%(i + ((pP | n) . n1m))%>) by Th7
.= (Product (i + (((pP | n) /^ n1) | m))) * (i + ((pP | n) . n1m)) by Th5 ;
set P = Product (i + (((pP | n) /^ n1) | m));
A33: pP = (pP | n) ^ <%(pP . n)%> by A28, AFINSQ_1:56;
A34: len ((pP | n) /^ n1) > m by A30, NAT_1:13;
A35: (pP /^ n1) | m = (((pP | n) /^ n1) ^ <%(pP . n)%>) | m by A33, Th10, A29, A12, XXREAL_0:2
.= ((pP | n) /^ n1) | m by AFINSQ_1:58, A34 ;
( pP . I1 = (pP | n) . i1 & pP . N1M = (pP | n) . n1m ) by A5, HILB10_3:4;
hence y in { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | (m + 1))) } by A26, A35, A32, A27; :: thesis: verum
end;
hence { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | (m + 1))) } is diophantine Subset of (n -xtuples_of NAT) by A11, A16, XBOOLE_0:def 10; :: thesis: verum
end;
A36: for m being Nat holds S1[m] from NAT_1:sch 2(A1, A3);
 let n be Nat; :: thesis: for i1 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | n2)) } is diophantine Subset of (n -xtuples_of NAT)
let i1 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | n2)) } is diophantine Subset of (n -xtuples_of NAT)
per cases ( n1 + n2 <= n or n1 + n2 > n ) ;
suppose n1 + n2 <= n ; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | n2)) } is diophantine Subset of (n -xtuples_of NAT)
hence { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | n2)) } is diophantine Subset of (n -xtuples_of NAT) by A36; :: thesis: verum
end;
suppose n1 + n2 > n ; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | n2)) } is diophantine Subset of (n -xtuples_of NAT)
then A37: n - n1 < n2 by XREAL_1:19;
per cases ( n1 >= n or n1 < n ) ;
suppose A38: n1 >= n ; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | n2)) } is diophantine Subset of (n -xtuples_of NAT)
defpred S2[ XFinSequence of NAT ] means $1 . i1 = Product (i + (($1 /^ n1) | n2));
defpred S3[ XFinSequence of NAT ] means $1 . i1 = 1;
A39: for p being n -element XFinSequence of NAT holds
( S2[p] iff S3[p] )
proof
let p be n -element XFinSequence of NAT ; :: thesis: ( S2[p] iff S3[p] )
len p = n by CARD_1:def 7;
then p /^ n1 = {} by A38, AFINSQ_2:6;
then i + ((p /^ n1) | n2) = {} ;
hence ( S2[p] iff S3[p] ) by Th4; :: thesis: verum
end;
{ p where p is n -element XFinSequence of NAT : S2[p] } = { q where q is n -element XFinSequence of NAT : S3[q] } from HILB10_3:sch 2(A39);
hence { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | n2)) } is diophantine Subset of (n -xtuples_of NAT) by HILB10_3:14; :: thesis: verum
end;
suppose A40: n1 < n ; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | n2)) } is diophantine Subset of (n -xtuples_of NAT)
then reconsider N = n - n1 as Nat by NAT_1:21;
defpred S2[ XFinSequence of NAT ] means $1 . i1 = Product (i + (($1 /^ n1) | n2));
defpred S3[ XFinSequence of NAT ] means $1 . i1 = Product (i + (($1 /^ n1) | N));
A41: for p being n -element XFinSequence of NAT holds
( S2[p] iff S3[p] )
proof
let p be n -element XFinSequence of NAT ; :: thesis: ( S2[p] iff S3[p] )
len p = n by CARD_1:def 7;
then len (p /^ n1) = n - n1 by A40, AFINSQ_2:7;
hence ( S2[p] iff S3[p] ) by A37, AFINSQ_1:52; :: thesis: verum
end;
A42: { p where p is n -element XFinSequence of NAT : S2[p] } = { q where q is n -element XFinSequence of NAT : S3[q] } from HILB10_3:sch 2(A41);
 n1 + N = n ;
hence { p where p is n -element XFinSequence of NAT : p . i1 = Product (i + ((p /^ n1) | n2)) } is diophantine Subset of (n -xtuples_of NAT) by A42, A36; :: thesis: verum
end;
end;
end;
end;