hilb10_4.miz

begin

 reserve i,j,n,n1,n2,m,k,l,u for Nat,

r,r1,r2 for Real,

x,y for Integer,

a,b for non trivial Nat,

F for XFinSequence,

cF,cF1,cF2 for complex-valued XFinSequence,

c,c1,c2 for Complex;

 registration

 let c1, c2;

 cluster <%c1, c2%> -> complex-valued;

 coherence

 proof

 c1 in COMPLEX & c2 in COMPLEX by XCMPLX_0:def 2;

 hence thesis;

 end;

 end

 definition

 let cF be XFinSequence;

 :: HILB10_4:def1

 func Product cF -> Element of COMPLEX equals ( multcomplex "**" cF);

 coherence ;

 end

 theorem :: HILB10_4:1



 Th1: cF is real-valued implies ( Product cF) = ( multreal "**" cF)

 proof

 assume

 A1: cF is real-valued;

 per cases by NAT_1: 14;

 suppose

 A2: ( len cF) = 0 ;



 hence ( multreal "**" cF) = ( the_unity_wrt multcomplex ) by BINOP_2: 6, BINOP_2: 7, AFINSQ_2:def 8, A1

 .= ( Product cF) by AFINSQ_2:def 8, A2;

 end;

 suppose

 A3: ( len cF) >= 1;



 A4: REAL = ( REAL /\ COMPLEX ) by MEMBERED: 1, XBOOLE_1: 28;

 now

 let x,y be object;

 assume x in REAL & y in REAL ;

 then

 reconsider X = x, Y = y as Element of REAL ;

 ( multreal . (x,y)) = (X * Y) by BINOP_2:def 11;

 hence ( multreal . (x,y)) = ( multcomplex . (x,y)) & ( multreal . (x,y)) in REAL by BINOP_2:def 5, XREAL_0:def 1;

 end;

 hence thesis by AFINSQ_2: 47, A3, A4, A1;

 end;

 end;

 theorem :: HILB10_4:2

 cF is INT -valued implies ( Product cF) = ( multint "**" cF)

 proof

 assume

 A1: cF is INT -valued;

 per cases by NAT_1: 14;

 suppose

 A2: ( len cF) = 0 ;



 hence ( multint "**" cF) = ( the_unity_wrt multcomplex ) by BINOP_2: 6, BINOP_2: 9, AFINSQ_2:def 8, A1

 .= ( Product cF) by AFINSQ_2:def 8, A2;

 end;

 suppose

 A3: ( len cF) >= 1;



 A4: INT = ( INT /\ COMPLEX ) by MEMBERED: 1, XBOOLE_1: 28;

 now

 let x,y be object;

 assume x in INT & y in INT ;

 then

 reconsider X = x, Y = y as Element of INT ;

 ( multint . (x,y)) = (X * Y) by BINOP_2:def 22;

 hence ( multint . (x,y)) = ( multcomplex . (x,y)) & ( multint . (x,y)) in INT by BINOP_2:def 5, INT_1:def 2;

 end;

 hence thesis by AFINSQ_2: 47, A3, A4, A1;

 end;

 end;

 theorem :: HILB10_4:3



 Th3: cF is natural-valued implies ( Product cF) = ( multnat "**" cF)

 proof

 assume cF is natural-valued;

 then ( rng cF) c= NAT by VALUED_0:def 6;

 then

 A1: cF is NAT -valued by RELAT_1:def 19;

 per cases by NAT_1: 14;

 suppose

 A2: ( len cF) = 0 ;



 hence ( multnat "**" cF) = ( the_unity_wrt multcomplex ) by BINOP_2: 6, BINOP_2: 10, AFINSQ_2:def 8, A1

 .= ( Product cF) by AFINSQ_2:def 8, A2;

 end;

 suppose

 A3: ( len cF) >= 1;



 A4: NAT = ( NAT /\ COMPLEX ) by MEMBERED: 1, XBOOLE_1: 28;

 now

 let x,y be object;

 assume x in NAT & y in NAT ;

 then

 reconsider X = x, Y = y as Element of NAT ;

 ( multnat . (x,y)) = (X * Y) by BINOP_2:def 24;

 hence ( multnat . (x,y)) = ( multcomplex . (x,y)) & ( multnat . (x,y)) in NAT by BINOP_2:def 5, ORDINAL1:def 12;

 end;

 hence thesis by AFINSQ_2: 47, A3, A4, A1;

 end;

 end;

 registration

 let F be real-valued XFinSequence;

 cluster ( Product F) -> real;

 coherence

 proof

 ( Product F) = ( multreal "**" F) by Th1;

 hence thesis;

 end;

 end

 registration

 let F be natural-valued XFinSequence;

 cluster ( Product F) -> natural;

 coherence

 proof

 ( Product F) = ( multnat "**" F) by Th3;

 hence thesis;

 end;

 end

 theorem :: HILB10_4:4



 Th4: cF = {} implies ( Product cF) = 1

 proof

 assume cF = {} ;

 then ( len cF) = 0 ;

 hence thesis by BINOP_2: 6, AFINSQ_2:def 8;

 end;

 theorem :: HILB10_4:5



 Th5: ( Product <%c%>) = c

 proof

 c in COMPLEX by XCMPLX_0:def 2;

 hence thesis by AFINSQ_2: 37;

 end;

 theorem :: HILB10_4:6

 ( Product <%c1, c2%>) = (c1 * c2)

 proof

 c1 in COMPLEX & c2 in COMPLEX by XCMPLX_0:def 2;



 then ( multcomplex "**" <%c1, c2%>) = ( multcomplex . (c1,c2)) by AFINSQ_2: 38

 .= (c1 * c2) by BINOP_2:def 5;

 hence thesis;

 end;

 theorem :: HILB10_4:7



 Th7: ( Product (cF1 ^ cF2)) = (( Product cF1) * ( Product cF2))

 proof



 thus ( Product (cF1 ^ cF2)) = ( multcomplex . (( Product cF1),( Product cF2))) by AFINSQ_2: 42

 .= (( Product cF1) * ( Product cF2)) by BINOP_2:def 5;

 end;

 theorem :: HILB10_4:8



 Th8: (c + (cF1 ^ cF2)) = ((c + cF1) ^ (c + cF2))

 proof



 A1: ( dom (c + cF1)) = ( dom cF1) & ( dom (c + cF2)) = ( dom cF2) & ( dom (c + (cF1 ^ cF2))) = ( dom (cF1 ^ cF2)) by VALUED_1:def 2;



 A2: ( len (cF1 ^ cF2)) = (( len cF1) + ( len cF2)) & ( len ((c + cF1) ^ (c + cF2))) = (( len (c + cF1)) + ( len (c + cF2))) by AFINSQ_1: 17;

 for x be object st x in ( dom (c + (cF1 ^ cF2))) holds ((c + (cF1 ^ cF2)) . x) = (((c + cF1) ^ (c + cF2)) . x)

 proof

 let x be object;

 assume

 A3: x in ( dom (c + (cF1 ^ cF2)));

 then

 reconsider i = x as Nat;

 per cases by A3, A1, AFINSQ_1: 20;

 suppose

 A4: i in ( dom cF1);

 then

 A5: ((cF1 ^ cF2) . i) = (cF1 . i) & (((c + cF1) ^ (c + cF2)) . i) = ((c + cF1) . i) by A1, AFINSQ_1:def 3;



 hence ((c + (cF1 ^ cF2)) . x) = (c + (cF1 . i)) by A3, VALUED_1:def 2

 .= (((c + cF1) ^ (c + cF2)) . x) by A5, A4, A1, VALUED_1:def 2;

 end;

 suppose ex n st n in ( dom cF2) & i = (( len cF1) + n);

 then

 consider n such that

 A6: n in ( dom cF2) & i = (( len cF1) + n);



 A7: ((cF1 ^ cF2) . i) = (cF2 . n) & (((c + cF1) ^ (c + cF2)) . i) = ((c + cF2) . n) by A1, A6, AFINSQ_1:def 3;



 hence ((c + (cF1 ^ cF2)) . x) = (c + (cF2 . n)) by A3, VALUED_1:def 2

 .= (((c + cF1) ^ (c + cF2)) . x) by A1, A6, A7, VALUED_1:def 2;

 end;

 end;

 hence thesis by A1, A2, FUNCT_1: 2;

 end;

 theorem :: HILB10_4:9



 Th9: (c1 + <%c2%>) = <%(c1 + c2)%>

 proof



 A1: ( dom <%(c1 + c2)%>) = 1 = ( dom <%c2%>) = ( dom (c1 + <%c2%>)) by VALUED_1:def 2, AFINSQ_1:def 4;

 ( <%(c1 + c2)%> . 0 ) = (c1 + ( <%c2%> . 0 ))

 .= ((c1 + <%c2%>) . 0 ) by A1, AFINSQ_1: 66, VALUED_1:def 2;

 hence thesis by A1, AFINSQ_1:def 4;

 end;

 theorem :: HILB10_4:10



 Th10: for f1,f2 be XFinSequence, n st n <= ( len f1) holds ((f1 ^ f2) /^ n) = ((f1 /^ n) ^ f2)

 proof

 let f1,f2 be XFinSequence, n;

 assume n <= ( len f1);

 then

 A2: ( len (f1 | n)) = n by AFINSQ_1: 54;

 f1 = ((f1 | n) ^ (f1 /^ n));

 then (f1 ^ f2) = ((f1 | n) ^ ((f1 /^ n) ^ f2)) by AFINSQ_1: 27;

 hence ((f1 ^ f2) /^ n) = ((f1 /^ n) ^ f2) by A2, AFINSQ_2: 12;

 end;

 registration

 let n;

 cluster n -element natural-valued for XFinSequence;

 existence

 proof

 take the n -element XFinSequence of NAT ;

 thus thesis;

 end;

 end

 registration

 cluster natural-valued positive-yielding for XFinSequence;

 existence

 proof

 take (( Segm the Nat) --> 1);

 thus thesis;

 end;

 end

 registration

 let R be positive-yielding Relation;

 let X be set;

 cluster (R | X) -> positive-yielding;

 coherence

 proof



 A1: ( rng (R | X)) c= ( rng R) by RELAT_1: 70;

 let r be Real;

 assume r in ( rng (R | X));

 hence thesis by A1, PARTFUN3:def 1;

 end;

 end

 registration

 let X be positive-yielding real-valued XFinSequence;

 cluster ( Product X) -> positive;

 coherence

 proof

 defpred P[ Nat] means for X be positive-yielding real-valued XFinSequence st ( len X) = $1 holds ( Product X) is positive;



 A1: P[ 0 ]

 proof

 let X be positive-yielding real-valued XFinSequence;

 assume ( len X) = 0 ;

 then X = {} ;

 hence thesis by Th4;

 end;



 A2: P[n] implies P[(n + 1)]

 proof

 set n1 = (n + 1);

 assume

 A3: P[n];

 let X be positive-yielding real-valued XFinSequence;

 set XX = <%(X . n)%>;

 assume

 A4: ( len X) = n1;

 then X = ((X | n) ^ <%(X . n)%>) by AFINSQ_1: 56;



 then

 A5: ( Product X) = (( Product (X | n)) * ( Product XX)) by Th7

 .= (( Product (X | n)) * (X . n)) by Th5;

 n < n1 by NAT_1: 13;

 then n in ( dom X) & ( len (X | n)) = n by A4, AFINSQ_1: 54, AFINSQ_1: 66;

 then

 A6: ( Product (X | n)) > 0 & (X . n) in ( rng X) by A3, FUNCT_1:def 3;

 then (X . n) > 0 by PARTFUN3:def 1;

 hence ( Product X) is positive by A5, A6;

 end;

 P[n] from NAT_1:sch 2( A1, A2);

 then P[( len X)];

 hence thesis;

 end;

 end

 theorem :: HILB10_4:11

 for X be natural-valued positive-yielding XFinSequence st i in ( dom X) holds (X . i) <= ( Product X)

 proof

 defpred P[ Nat] means for X be natural-valued positive-yielding XFinSequence, i be Nat st ( len X) = $1 & i in ( dom X) holds (X . i) <= ( Product X);



 A1: P[ 0 ] by XBOOLE_0:def 1;



 A2: P[n] implies P[(n + 1)]

 proof

 set n1 = (n + 1);

 assume

 A3: P[n];

 let X be positive-yielding natural-valued XFinSequence, i be Nat;

 assume

 A4: ( len X) = n1 & i in ( dom X);

 then X = ((X | n) ^ <%(X . n)%>) by AFINSQ_1: 56;



 then

 A5: ( Product X) = (( Product (X | n)) * ( Product <%(X . n)%>)) by Th7

 .= (( Product (X | n)) * (X . n)) by Th5;



 A6: n < n1 by NAT_1: 13;

 then

 A7: n in ( dom X) & ( len (X | n)) = n by A4, AFINSQ_1: 54, AFINSQ_1: 66;

 then ( Product (X | n)) > 0 & (X . n) in ( rng X) by FUNCT_1:def 3;

 then

 A8: (X . n) > 0 & ( Product (X | n)) >= 1 by PARTFUN3:def 1, NAT_1: 14;

 then

 A9: (X . n) >= 1 by NAT_1: 14;

 i < ( len X) by A4, AFINSQ_1: 66;

 then i <= n by A4, NAT_1: 13;

 per cases by XXREAL_0: 1;

 suppose i = n;

 then ( Product X) >= ((X . i) * 1) by A5, A8, XREAL_1: 66;

 hence thesis;

 end;

 suppose

 A10: i < n;

 then

 A11: i in ( dom (X | n)) by A7, AFINSQ_1: 66;

 ( Product (X | n)) >= ((X | n) . i) by A3, A7, AFINSQ_1: 66, A10;

 then ( Product X) >= (((X | n) . i) * 1) & ((X | n) . i) = (X . i) by A6, A4, AFINSQ_1: 53, A11, A7, A5, A9, XREAL_1: 66;

 hence thesis;

 end;

 end;



 A12: P[n] from NAT_1:sch 2( A1, A2);

 let X be natural-valued positive-yielding XFinSequence;

 thus thesis by A12;

 end;

 registration

 let X be natural-valued XFinSequence, n be positive Nat;

 cluster (n + X) -> positive-yielding;

 coherence

 proof

 now

 let r be Real;

 assume r in ( rng (n + X));

 then

 consider x be object such that

 A1: x in ( dom (n + X)) & ((n + X) . x) = r by FUNCT_1:def 3;

 ((n + X) . x) = (n + (X . x)) by A1, VALUED_1:def 2;

 hence r > 0 by A1;

 end;

 hence thesis by PARTFUN3:def 1;

 end;

 end

 theorem :: HILB10_4:12

 for X1,X2 be natural-valued XFinSequence st ( len X1) = ( len X2) & for n st n in ( dom X1) holds (X1 . n) <= (X2 . n) holds ( Product X1) <= ( Product X2)

 proof

 defpred P[ Nat] means for X1,X2 be natural-valued XFinSequence st ( len X1) = $1 = ( len X2) & for n st n in ( dom X1) holds (X1 . n) <= (X2 . n) holds ( Product X1) <= ( Product X2);



 A1: P[ 0 ]

 proof

 let X1,X2 be natural-valued XFinSequence;

 assume ( len X1) = 0 = ( len X2);

 then X1 = {} = X2;

 hence thesis;

 end;



 A2: P[n] implies P[(n + 1)]

 proof

 set n1 = (n + 1);

 assume

 A3: P[n];

 let X1,X2 be natural-valued XFinSequence;

 assume that

 A4: ( len X1) = n1 = ( len X2) and

 A5: for i st i in ( dom X1) holds (X1 . i) <= (X2 . i);

 X1 = ((X1 | n) ^ <%(X1 . n)%>) by A4, AFINSQ_1: 56;



 then

 A6: ( Product X1) = (( Product (X1 | n)) * ( Product <%(X1 . n)%>)) by Th7

 .= (( Product (X1 | n)) * (X1 . n)) by Th5;

 X2 = ((X2 | n) ^ <%(X2 . n)%>) by A4, AFINSQ_1: 56;



 then

 A7: ( Product X2) = (( Product (X2 | n)) * ( Product <%(X2 . n)%>)) by Th7

 .= (( Product (X2 | n)) * (X2 . n)) by Th5;



 A8: n < n1 by NAT_1: 13;

 then

 A9: n in ( dom X1) & ( len (X1 | n)) = n = ( len (X2 | n)) by A4, AFINSQ_1: 54, AFINSQ_1: 66;



 A10: (X1 . n) <= (X2 . n) by A5, A8, A4, AFINSQ_1: 66;

 for i st i in ( dom (X1 | n)) holds ((X1 | n) . i) <= ((X2 | n) . i)

 proof

 let i;

 assume i in ( dom (X1 | n));

 then ((X1 | n) . i) = (X1 . i) & ((X2 | n) . i) = (X2 . i) & i in ( dom X1) by A8, A4, A9, AFINSQ_1: 53;

 hence thesis by A5;

 end;

 then ( Product (X1 | n)) <= ( Product (X2 | n)) by A3, A9;

 hence thesis by A6, A7, A10, XREAL_1: 66;

 end;

 P[n] from NAT_1:sch 2( A1, A2);

 hence thesis;

 end;

 begin

 theorem :: HILB10_4:13



 Th13: k <= n implies (n choose k) <= (n |^ k)

 proof

 defpred P[ Nat] means $1 <= n implies (n choose $1) <= (n |^ $1);

 (n choose 0 ) = 1 by NEWTON: 19;

 then

 A1: P[ 0 ] by NEWTON: 4;



 A2: P[m] implies P[(m + 1)]

 proof

 assume

 A3: P[m];

 set m1 = (m + 1);

 assume

 A4: m1 <= n;

 then m < n by NAT_1: 13;

 then

 A5: (n - m) > (m - m) by XREAL_1: 14;



 A6: (n - m) <= (n - 0 ) by XREAL_1: 10;



 A7: (n choose m1) = (((n - m) / m1) * (n choose m)) by IRRAT_1: 5;

 ((n - m) / m1) <= ((n - m) / 1) by A5, XREAL_1: 118, NAT_1: 11;

 then ((n - m) / m1) <= n by A6, XXREAL_0: 2;

 then

 A8: (n choose m1) <= (n * (n choose m)) by A7, XREAL_1: 64;

 (n * (n choose m)) <= (n * (n |^ m)) by A3, A4, NAT_1: 13, XREAL_1: 64;

 then (n choose m1) <= (n * (n |^ m)) by A8, XXREAL_0: 2;

 hence thesis by NEWTON: 6;

 end;

 P[m] from NAT_1:sch 2( A1, A2);

 hence thesis;

 end;

 theorem :: HILB10_4:14



 Th14: u > (n |^ k) & n >= k & k > i implies ((n choose i) * (u |^ i)) < ((u |^ k) / n)

 proof

 assume

 A1: u > (n |^ k) & n >= k & k > i;

 then

 A2: k >= (i + 1) by NAT_1: 13;



 A3: u >= 1 by A1, NAT_1: 14;



 A4: n > 0 by A1;

 then n >= 1 by NAT_1: 14;

 then (n |^ (i + 1)) <= (n |^ k) by A2, PREPOWER: 93;

 then (n |^ (i + 1)) < u by A1, XXREAL_0: 2;

 then

 A5: ((n |^ (i + 1)) * (u |^ i)) < (u * (u |^ i)) by XREAL_1: 68;

 (u * (u |^ i)) = (u |^ (i + 1)) by NEWTON: 6;

 then (u * (u |^ i)) <= (u |^ k) by A3, A2, PREPOWER: 93;

 then ((n |^ (i + 1)) * (u |^ i)) < (u |^ k) & (n |^ (i + 1)) = (n * (n |^ i)) by A5, XXREAL_0: 2, NEWTON: 6;

 then (n * ((n |^ i) * (u |^ i))) < (u |^ k);

 then

 A6: ((n |^ i) * (u |^ i)) < ((u |^ k) / n) by A4, XREAL_1: 81;

 i <= n by A1, XXREAL_0: 2;

 then (n choose i) <= (n |^ i) by Th13;

 then ((n choose i) * (u |^ i)) <= ((n |^ i) * (u |^ i)) by XREAL_1: 64;

 hence thesis by A6, XXREAL_0: 2;

 end;

 theorem :: HILB10_4:15



 Th15: u > (n |^ k) & n >= k implies ( [\(((u + 1) |^ n) / (u |^ k))/] mod u) = (n choose k)

 proof

 assume

 A1: u > (n |^ k) & n >= k;

 set I = ((1,u) In_Power n), k1 = (k + 1);

 consider q be FinSequence such that

 A2: I = ((I | k1) ^ q) by FINSEQ_1: 80;

 ( rng I) c= NAT by VALUED_0:def 6;

 then

 reconsider I1 = I as FinSequence of NAT by FINSEQ_1:def 4;

 I1 = ((I1 | k1) ^ q) by A2;

 then

 reconsider q as FinSequence of NAT by FINSEQ_1: 36;



 A3: ( len I1) = (n + 1) by NEWTON:def 4;



 A4: ( len (I1 | k1)) = k1 by A1, XREAL_1: 7, A3, FINSEQ_1: 59;

 1 <= k1 by NAT_1: 11;

 then k1 in ( dom I) by A3, A1, XREAL_1: 7, FINSEQ_3: 25;

 then

 A5: (I1 | k1) = ((I1 | k) ^ <*(I1 . k1)*>) by FINSEQ_5: 10;



 A6: ( Sum I1) = (( Sum (I1 | k1)) + ( Sum q)) by A2, RVSUM_1: 75

 .= ((( Sum (I1 | k)) + (I1 . k1)) + ( Sum q)) by A5, RVSUM_1: 74;

 k <= (n + 1) by A1, NAT_1: 13;

 then

 A7: (I1 | k) is k -element by A3, FINSEQ_1: 59;

 set kI = (k |-> ((u |^ k) / n));



 A8: for i be Nat st i in ( Seg k) holds ((I1 | k) . i) < (kI . i)

 proof

 let i be Nat such that

 A9: i in ( Seg k);



 A10: (kI . i) = ((u |^ k) / n) by A9, FINSEQ_2: 57;



 A11: 1 <= i <= k by A9, FINSEQ_1: 1;

 then

 A12: ((I1 | k) . i) = (I1 . i) by FINSEQ_3: 112;

 reconsider i1 = (i - 1) as Nat by A11;

 set ni = (n -' i1);



 A13: (i1 + 1) = i & i <= n by A11, A1, XXREAL_0: 2;

 then

 A14: i1 < n & i <= (n + 1) by NAT_1: 13;

 then

 A15: i in ( dom I1) by A11, A3, FINSEQ_3: 25;

 ni = (n - i1) by A14, XREAL_1: 233;

 then

 A16: (I1 . i) = (((n choose i1) * (1 |^ ni)) * (u |^ i1)) by A15, NEWTON:def 4;

 k > i1 by A13, A11, NAT_1: 13;

 hence thesis by Th14, A1, A10, A16, A12;

 end;

 then

 A17: for i be Nat st i in ( Seg k) holds ((I1 | k) . i) <= (kI . i);

 1 <= k1 by NAT_1: 11;

 then

 A18: k1 in ( dom I1) by A1, XREAL_1: 7, A3, FINSEQ_3: 25;

 (n - k) = (n -' k) & k = (k1 - 1) by A1, XREAL_1: 233;

 then

 A19: (I1 . k1) = (((n choose k) * (1 |^ (n -' k))) * (u |^ k)) by A18, NEWTON:def 4;

 defpred P[ Nat, object] means $2 in NAT & for i be Nat st i = $2 holds (q . $1) = (((u |^ k) * u) * i);

 ( len I) = (k1 + ( len q)) by A2, A4, FINSEQ_1: 22;

 then

 A20: n = (k + ( len q)) by A3;



 A21: for j be Nat st j in ( Seg ( len q)) holds ex x be object st P[j, x]

 proof

 let j be Nat such that

 A22: j in ( Seg ( len q));



 A23: 1 <= j <= ( len q) by FINSEQ_1: 1, A22;



 A24: ((k1 + j) - 1) = (k + j);



 A25: n >= (k + j) by A23, A20, XREAL_1: 7;



 A26: (n -' (k + j)) = (n - (k + j)) by XREAL_1: 233, A23, A20, XREAL_1: 7;

 1 <= ((k + j) + 1) <= (n + 1) by NAT_1: 11, A25, XREAL_1: 7;

 then (k1 + j) in ( dom I1) by FINSEQ_3: 25, A3;

 then

 A27: (I1 . (k1 + j)) = (((n choose (k + j)) * (1 |^ (n -' (k + j)))) * (u |^ (k + j))) by A24, A26, NEWTON:def 4;

 reconsider j1 = (j - 1) as Nat by A23;



 A28: (u |^ (k + j)) = ((u |^ k) * (u |^ (j1 + 1))) by NEWTON: 8

 .= ((u |^ k) * ((u |^ j1) * u)) by NEWTON: 6;

 take U = (((n choose (k + j)) * (1 |^ (n -' (k + j)))) * (u |^ j1));

 thus thesis by A27, A28, A23, FINSEQ_1: 65, A2, A4, ORDINAL1:def 12;

 end;

 consider Q be FinSequence such that

 A29: ( dom Q) = ( Seg ( len q)) and

 A30: for j be Nat st j in ( Seg ( len q)) holds P[j, (Q . j)] from FINSEQ_1:sch 1( A21);

 ( rng Q) c= NAT

 proof

 let y be object such that

 A31: y in ( rng Q);

 ex x be object st x in ( dom Q) & (Q . x) = y by FUNCT_1:def 3, A31;

 hence thesis by A30, A29;

 end;

 then

 reconsider Q as FinSequence of NAT by FINSEQ_1:def 4;



 A32: ( len Q) = ( len q) & ( len (((u |^ k) * u) * Q)) = ( len Q) by CARD_1:def 7, A29, FINSEQ_1:def 3;

 for i be Nat st 1 <= i <= ( len q) holds (q . i) = ((((u |^ k) * u) * Q) . i)

 proof

 let i be Nat;

 assume 1 <= i <= ( len q);

 then i in ( dom Q) by A29;

 then (q . i) = (((u |^ k) * u) * (Q . i)) by A29, A30;

 hence thesis by VALUED_1: 6;

 end;

 then q = (((u |^ k) * u) * Q) by A32, FINSEQ_1: 14;

 then

 A33: ( Sum q) = (((u |^ k) * u) * ( Sum Q)) by RVSUM_1: 87;



 A34: [\(( Sum I1) / (u |^ k))/] = ((n choose k) + (u * ( Sum Q)))

 proof

 per cases by NAT_1: 14;

 suppose k = 0 ;

 then ( Sum (I1 | k)) = 0 by RVSUM_1: 72;

 then (1 * ( Sum I1)) = ((u |^ k) * ((n choose k) + (u * ( Sum Q)))) by A33, A19, A6;

 then (( Sum I1) / (u |^ k)) = (((n choose k) + (u * ( Sum Q))) / 1) by A1, XCMPLX_1: 94;

 hence thesis by INT_1: 25;

 end;

 suppose

 A35: k >= 1;

 then

 A36: k in ( Seg k);

 then

 A37: ((I1 | k) . k) < (kI . k) by A8;



 A38: ( Sum kI) = (k * ((u |^ k) / n)) by RVSUM_1: 80

 .= ((u |^ k) * (k / n)) by XCMPLX_1: 75;

 ( Sum (I1 | k)) < ((u |^ k) * (k / n)) by A37, A36, A7, A17, RVSUM_1: 83, A38;

 then

 A39: (( Sum (I1 | k)) + ((I1 . k1) + ( Sum q))) < (((u |^ k) * (k / n)) + ((I1 . k1) + ( Sum q))) by XREAL_1: 8;

 (((u |^ k) * (k / n)) + ((I1 . k1) + ( Sum q))) = ((u |^ k) * (((k / n) + (n choose k)) + (u * ( Sum Q)))) by A33, A19;

 then

 A40: (( Sum I1) / (u |^ k)) < (((k / n) + (n choose k)) + (u * ( Sum Q))) by A1, A39, A6, XREAL_1: 83;

 (k / n) <= (n / n) & (n / n) = 1 by A35, XREAL_1: 72, A1, XCMPLX_1: 60;

 then ((k / n) + ((n choose k) + (u * ( Sum Q)))) <= (1 + ((n choose k) + (u * ( Sum Q)))) by XREAL_1: 7;

 then (( Sum I1) / (u |^ k)) < (1 + ((n choose k) + (u * ( Sum Q)))) by A40, XXREAL_0: 2;

 then

 A41: ((( Sum I1) / (u |^ k)) - 1) < ((n choose k) + (u * ( Sum Q))) by XREAL_1: 19;



 A42: ( 0 + ((I1 . k1) + ( Sum q))) <= (( Sum (I1 | k)) + ((I1 . k1) + ( Sum q))) by XREAL_1: 7;

 ((I1 . k1) + ( Sum q)) = ((u |^ k) * ((n choose k) + (u * ( Sum Q)))) by A33, A19;

 then (( Sum I1) / (u |^ k)) >= ((n choose k) + (u * ( Sum Q))) by A1, A42, A6, XREAL_1: 77;

 hence thesis by A41, INT_1:def 6;

 end;

 end;



 A43: ( Sum I1) = ((1 + u) |^ n) by NEWTON: 30;

 (n choose k) <= (n |^ k) by Th13, A1;

 then (n choose k) < u by A1, XXREAL_0: 2;

 then ((n choose k) mod u) = (n choose k) by NAT_D: 24;

 hence thesis by A34, A43, NAT_D: 21;

 end;

 theorem :: HILB10_4:16



 Th16: for x,y,z be Nat holds x >= z & y = (x choose z) iff ex u,v,y1,y2,y3 be Nat st y1 = (x |^ z) & y2 = ((u + 1) |^ x) & y3 = (u |^ z) & u > y1 & v = [\(y2 / y3)/] & (y,v) are_congruent_mod u & y = z

 proof

 let x,y,z be Nat;

 thus x >= z & y = (x choose z) implies ex u,v,y1,y2,y3 be Nat st y1 = (x |^ z) & y2 = ((u + 1) |^ x) & y3 = (u |^ z) & u > y1 & v = [\(y2 / y3)/] & (y,v) are_congruent_mod u & y = z

 proof

 assume

 A1: x >= z & y = (x choose z);

 set y1 = (x |^ z), u = (y1 + 1), y2 = ((u + 1) |^ x), y3 = (u |^ z), v = [\(y2 / y3)/];

 reconsider v as Element of NAT by INT_1: 3, INT_1: 54;

 take u, v, y1, y2, y3;

 thus

 A2: y1 = (x |^ z) & y2 = ((u + 1) |^ x) & y3 = (u |^ z) & u > y1 & v = [\(y2 / y3)/] by NAT_1: 13;



 A3: (v mod u) = y by A2, Th15, A1;

 y < u by A1, NAT_1: 13, Th13;

 then (y mod u) = y by NAT_D: 24;

 then ((y - v) mod u) = 0 by A3, INT_4: 22;

 then u divides (y - v) by INT_1: 62;

 hence thesis by A1, NAT_1: 13, Th13, INT_1:def 4;

 end;

 given u,v,y1,y2,y3 be Nat such that

 A4: y1 = (x |^ z) & y2 = ((u + 1) |^ x) & y3 = (u |^ z) and

 A5: u > y1 & v = [\(y2 / y3)/] & (y,v) are_congruent_mod u and

 A6: y = z;

 u divides (y - v) by A5, INT_1:def 4;

 then ((y - v) mod u) = 0 by INT_1: 62, A5;

 then (y mod u) = (v mod u) by INT_4: 22, A5;

 then (y mod u) = (x choose z) by Th15, A4, A5, A6;

 hence thesis by A6, NAT_D: 24;

 end;

 begin



 Lm1: k < n implies (1 - (k / n)) = ((n - k) / n) & (1 / (1 - (k / n))) = (n / (n - k))

 proof

 assume k < n;



 then (1 - (k / n)) = ((n / n) - (k / n)) by XCMPLX_1: 60

 .= ((n - k) / n) by XCMPLX_1: 120;

 hence thesis by XCMPLX_1: 57;

 end;



 Lm2: for n, k st k < n holds ((n |^ k) / (n choose k)) <= (((k ! ) * 1) / ((1 - (k / n)) |^ k))

 proof

 let n;

 defpred P[ Nat] means $1 < n implies ((n |^ $1) / (n choose $1)) <= ((($1 ! ) * 1) / ((1 - ($1 / n)) |^ $1));

 (n |^ 0 ) = 1 & (n choose 0 ) = 1 by NEWTON: 4, NEWTON: 19;

 then

 A1: P[ 0 ] by NEWTON: 12;



 A2: for k st P[k] holds P[(k + 1)]

 proof

 let k such that

 A3: P[k];

 set k1 = (k + 1);

 assume

 A4: k1 < n;



 A5: ((n |^ k1) / (n choose k1)) = ((n |^ k1) / (((n - k) / (k + 1)) * (n choose k))) by IRRAT_1: 5

 .= (((n |^ k1) / (n choose k)) / ((n - k) / k1)) by XCMPLX_1: 78

 .= (((n |^ k1) / (n choose k)) * (k1 / (n - k))) by XCMPLX_1: 79

 .= (((n * (n |^ k)) / (n choose k)) * (k1 / (n - k))) by NEWTON: 6

 .= ((((n |^ k) / (n choose k)) * n) * (k1 / (n - k))) by XCMPLX_1: 74

 .= (((n |^ k) / (n choose k)) * (n * (k1 / (n - k))));

 k < n by A4, NAT_1: 13;

 then

 A6: (n - k) > 0 & (n - k1) > 0 by XREAL_1: 50, A4;

 k < k1 by NAT_1: 13;

 then (k / n) < (k1 / n) by A4, XREAL_1: 74;

 then

 A7: (1 - (k / n)) > (1 - (k1 / n)) by XREAL_1: 10;



 A8: (1 - (k1 / n)) = ((n - k1) / n) by Lm1, A4;

 then

 A9: ((1 - (k / n)) |^ k1) > ((1 - (k1 / n)) |^ k1) by NAT_1: 11, A7, A6, PREPOWER: 10;



 A10: k < n by A4, NAT_1: 13;



 A11: ((n |^ k1) / (n choose k1)) <= ((((k ! ) * 1) / ((1 - (k / n)) |^ k)) * (n * (k1 / (n - k)))) by A3, A5, XREAL_1: 64, A6, A4, NAT_1: 13;



 A12: ((1 / ((1 - (k / n)) |^ k)) * (n / (n - k))) = ((1 / ((1 - (k / n)) |^ k)) * (1 / (1 - (k / n)))) by A10, Lm1

 .= ((1 * 1) / (((1 - (k / n)) |^ k) * (1 - (k / n)))) by XCMPLX_1: 76

 .= (1 / ((1 - (k / n)) |^ k1)) by NEWTON: 6;



 A13: ((((k ! ) * 1) / ((1 - (k / n)) |^ k)) * (n * (k1 / (n - k)))) = ((((k ! ) * 1) / ((1 - (k / n)) |^ k)) * (k1 * (n / (n - k)))) by XCMPLX_1: 75

 .= (((k ! ) * (1 / ((1 - (k / n)) |^ k))) * (k1 * (n / (n - k)))) by XCMPLX_1: 74

 .= ((((k ! ) * k1) * (1 / ((1 - (k / n)) |^ k))) * (n / (n - k)))

 .= (((k1 ! ) * (1 / ((1 - (k / n)) |^ k))) * (n / (n - k))) by NEWTON: 15

 .= ((k1 ! ) * (1 / ((1 - (k / n)) |^ k1))) by A12

 .= (((k1 ! ) * 1) / ((1 - (k / n)) |^ k1)) by XCMPLX_1: 74;

 (((k1 ! ) * 1) / ((1 - (k / n)) |^ k1)) < (((k1 ! ) * 1) / ((1 - (k1 / n)) |^ k1)) by A8, A6, A4, A9, XREAL_1: 76;

 hence thesis by A11, A13, XXREAL_0: 2;

 end;

 for k holds P[k] from NAT_1:sch 2( A1, A2);

 hence thesis;

 end;



 Lm3: 0 < (2 * k) < n implies (1 / (1 - (k / n))) <= (1 + ((2 * k) / n))

 proof

 assume

 A1: 0 < (2 * k) < n;

 k <= (k + k) by NAT_1: 11;

 then

 A2: k < n by A1, XXREAL_0: 2;

 then

 A3: (n - k) > 0 by XREAL_1: 50;



 A4: k > 0 by A1;

 (n * k) > ((2 * k) * k) by A4, A1, XREAL_1: 68;

 then 0 < ((n * k) - ((2 * k) * k)) by XREAL_1: 50;

 then ((n * n) + 0 ) < ((n * n) + ((((2 * n) * k) - (k * n)) - ((2 * k) * k))) by XREAL_1: 6;

 then (n * n) < ((n + (2 * k)) * (n - k));

 then

 A5: (n / (n - k)) < ((n + (2 * k)) / n) by A1, A3, XREAL_1: 106;

 ((n + (2 * k)) / n) = ((n / n) + ((2 * k) / n)) by XCMPLX_1: 62

 .= (1 + ((2 * k) / n)) by A1, XCMPLX_1: 60;

 hence thesis by A5, A2, Lm1;

 end;



 Lm4: for n, k st k < n holds (k ! ) <= ((n |^ k) / (n choose k))

 proof

 let n;

 defpred P[ Nat] means $1 < n implies ($1 ! ) <= ((n |^ $1) / (n choose $1));

 (n |^ 0 ) = 1 & (n choose 0 ) = 1 by NEWTON: 4, NEWTON: 19;

 then

 A1: P[ 0 ] by NEWTON: 12;



 A2: for k st P[k] holds P[(k + 1)]

 proof

 let k such that

 A3: P[k];

 set k1 = (k + 1);

 assume

 A4: k1 < n;

 then

 A5: k < n by NAT_1: 13;



 A6: ((n |^ k1) / (n choose k1)) = ((n |^ k1) / (((n - k) / (k + 1)) * (n choose k))) by IRRAT_1: 5

 .= (((n |^ k1) / (n choose k)) / ((n - k) / k1)) by XCMPLX_1: 78

 .= (((n |^ k1) / (n choose k)) * (k1 / (n - k))) by XCMPLX_1: 79

 .= (((n * (n |^ k)) / (n choose k)) * (k1 / (n - k))) by NEWTON: 6

 .= ((((n |^ k) / (n choose k)) * n) * (k1 / (n - k))) by XCMPLX_1: 74

 .= (((n |^ k) / (n choose k)) * (n * (k1 / (n - k))));



 A7: n >= (n - k) by XREAL_1: 43;

 (n - k) > 0 by A5, XREAL_1: 50;

 then (n / (n - k)) >= 1 by A7, XREAL_1: 181;

 then

 A8: (k1 * (n / (n - k))) >= (k1 * 1) by XREAL_1: 64;

 (k1 * (n / (n - k))) = ((n * k1) / (n - k)) by XCMPLX_1: 74

 .= (n * (k1 / (n - k))) by XCMPLX_1: 74;

 then (((n |^ k) / (n choose k)) * (n * (k1 / (n - k)))) >= ((k ! ) * k1) by A4, NAT_1: 13, A3, A8, XREAL_1: 66;

 hence thesis by A6, NEWTON: 15;

 end;

 for k holds P[k] from NAT_1:sch 2( A1, A2);

 hence thesis;

 end;



 Lm5: 0 < r < (1 / 2) implies ((1 + r) |^ k) < (1 + (r * (2 |^ k)))

 proof

 assume

 A1: 0 < r < (1 / 2);

 defpred P[ Nat] means ((1 + r) |^ $1) < (1 + (r * (2 |^ $1)));

 per cases by NAT_1: 14;

 suppose

 A2: k = 0 ;

 ((1 + r) |^ 0 ) = 1 & (2 |^ 0 ) = 1 & (1 + 0 ) < (1 + r) by NEWTON: 4, A1, XREAL_1: 8;

 hence thesis by A2;

 end;

 suppose

 A3: k >= 1;

 ((1 + r) + 0 ) < ((1 + r) + r) by A1, XREAL_1: 8;

 then

 A4: P[1];



 A5: for k st 1 <= k holds P[k] implies P[(k + 1)]

 proof

 let k such that

 A6: 1 <= k and

 A7: P[k];

 set k1 = (k + 1);

 (2 |^ k) >= 2 by A6, PREPOWER: 12;

 then

 A8: ((2 |^ k) * (1 / 2)) >= (2 * (1 / 2)) by XREAL_1: 64;

 (r * (2 |^ k)) < ((1 / 2) * (2 |^ k)) by A1, XREAL_1: 68;

 then (1 + (r * (2 |^ k))) < (((1 / 2) * (2 |^ k)) + ((1 / 2) * (2 |^ k))) by A8, XREAL_1: 8;

 then

 A9: ((2 |^ k) + (1 + (r * (2 |^ k)))) < ((2 |^ k) + (2 |^ k)) by XREAL_1: 8;

 (2 |^ k1) = (2 * (2 |^ k)) by NEWTON: 6;

 then (r * (((2 |^ k) + 1) + (r * (2 |^ k)))) < (r * (2 |^ k1)) by A9, A1, XREAL_1: 68;

 then

 A10: (1 + (r * (((2 |^ k) + 1) + (r * (2 |^ k))))) < (1 + (r * (2 |^ k1))) by XREAL_1: 8;



 A11: ((1 + r) |^ k1) = (((1 + r) |^ k) * (1 + r)) by NEWTON: 6;

 ((1 + r) |^ k1) < ((1 + (r * (2 |^ k))) * (1 + r)) by A7, A1, A11, XREAL_1: 68;

 hence thesis by A10, XXREAL_0: 2;

 end;

 for k st 1 <= k holds P[k] from NAT_1:sch 8( A4, A5);

 hence thesis by A3;

 end;

 end;

 theorem :: HILB10_4:17



 Th17: k > 0 & n > ((2 * k) |^ (k + 1)) implies (k ! ) = [\((n |^ k) / (n choose k))/]

 proof

 set k1 = (k + 1);

 assume

 A1: k > 0 & n > ((2 * k) |^ k1);



 A2: (2 * k) >= 1 & k >= 1 by A1, NAT_1: 14;

 k1 >= 1 by NAT_1: 11;

 then ((2 * k) |^ k1) >= (2 * k) by A2, PREPOWER: 12;

 then

 A3: n > (2 * k) by A1, XXREAL_0: 2;

 k1 > (1 + 0 ) by A1, XREAL_1: 6;

 then k1 >= (1 + 1) by NAT_1: 13;

 then

 A4: ((2 * k) |^ k1) >= ((2 * k) |^ (1 + 1)) by A1, NAT_6: 1;

 ((2 * k) |^ (1 + 1)) = (((2 * k) |^ 1) * (2 * k)) by NEWTON: 6

 .= ((2 * k) * (2 * k));

 then

 A5: n > ((4 * k) * k) by A1, A4, XXREAL_0: 2;

 ((4 * k) * k) >= ((4 * k) * 1) by A1, NAT_1: 14, XREAL_1: 64;

 then

 A6: (1 * n) > (2 * (2 * k)) by A5, XXREAL_0: 2;

 (k + k) >= k by NAT_1: 11;

 then

 A7: n > k by A3, XXREAL_0: 2;

 then

 A8: ((n |^ k) / (n choose k)) <= (((k ! ) * 1) / ((1 - (k / n)) |^ k)) by Lm2;



 A9: (1 / ((1 - (k / n)) |^ k)) = ((1 / (1 - (k / n))) |^ k) by PREPOWER: 7;



 A10: (n - k) > 0 by A7, XREAL_1: 50;



 A11: (1 / (1 - (k / n))) = (n / (n - k)) by A7, Lm1;

 (1 / (1 - (k / n))) <= (1 + ((2 * k) / n)) by A1, A3, Lm3;

 then

 A12: (1 / ((1 - (k / n)) |^ k)) <= ((1 + ((2 * k) / n)) |^ k) by A9, A11, A1, A10, PREPOWER: 9;

 ((1 + ((2 * k) / n)) |^ k) < (1 + (((2 * k) / n) * (2 |^ k))) by A6, XREAL_1: 106, A1, Lm5;

 then (1 / ((1 - (k / n)) |^ k)) < (1 + (((2 * k) / n) * (2 |^ k))) by A12, XXREAL_0: 2;

 then ((k ! ) * (1 / ((1 - (k / n)) |^ k))) < ((k ! ) * (1 + (((2 * k) / n) * (2 |^ k)))) by XREAL_1: 68;

 then (((k ! ) * 1) / ((1 - (k / n)) |^ k)) < ((k ! ) * (1 + (((2 * k) / n) * (2 |^ k)))) by XCMPLX_1: 74;

 then

 A13: ((n |^ k) / (n choose k)) < ((k ! ) * (1 + (((2 * k) / n) * (2 |^ k)))) by A8, XXREAL_0: 2;

 (((2 * k) / n) * (2 |^ k)) = (((2 * k) * (2 |^ k)) / n) by XCMPLX_1: 74;



 then

 A14: (((k ! ) * ((2 * k) / n)) * (2 |^ k)) = ((k ! ) * (((2 * k) * (2 |^ k)) / n))

 .= (((k ! ) * ((2 * k) * (2 |^ k))) / n) by XCMPLX_1: 74

 .= ((((k ! ) * (2 * k)) * (2 |^ k)) / n);

 ((((k ! ) * (2 * k)) * (2 |^ k)) / n) < ((((k ! ) * (2 * k)) * (2 |^ k)) / ((2 * k) |^ k1)) by A1, XREAL_1: 76;

 then ((k ! ) + ((((k ! ) * (2 * k)) * (2 |^ k)) / n)) < ((k ! ) + ((((k ! ) * (2 * k)) * (2 |^ k)) / ((2 * k) |^ k1))) by XREAL_1: 6;

 then

 A15: ((n |^ k) / (n choose k)) < ((k ! ) + ((((k ! ) * (2 * k)) * (2 |^ k)) / ((2 * k) |^ k1))) by A13, XXREAL_0: 2, A14;



 A16: ((2 * k) * (2 |^ k)) = (k * (2 * (2 |^ k)))

 .= (k * (2 |^ k1)) by NEWTON: 6;



 A17: (((2 * k) * (2 |^ k)) / ((2 * k) |^ k1)) = ((k * (2 |^ k1)) / ((2 |^ k1) * (k |^ k1))) by A16, NEWTON: 7

 .= (k / (k |^ k1)) by XCMPLX_1: 91

 .= (k / (k * (k |^ k))) by NEWTON: 6;



 A18: ((((k ! ) * (2 * k)) * (2 |^ k)) / ((2 * k) |^ k1)) = (((k ! ) * ((2 * k) * (2 |^ k))) / ((2 * k) |^ k1))

 .= ((k ! ) * (k / (k * (k |^ k)))) by A17, XCMPLX_1: 74

 .= (((k ! ) * k) / (k * (k |^ k))) by XCMPLX_1: 74

 .= ((k ! ) / (k |^ k)) by A1, XCMPLX_1: 91;

 ((k ! ) / (k |^ k)) <= 1 by XREAL_1: 183, NEWTON02: 124;

 then ((k ! ) + ((((k ! ) * (2 * k)) * (2 |^ k)) / ((2 * k) |^ k1))) <= ((k ! ) + 1) by A18, XREAL_1: 6;

 then ((n |^ k) / (n choose k)) < ((k ! ) + 1) by A15, XXREAL_0: 2;

 then

 A19: (((n |^ k) / (n choose k)) - 1) < (k ! ) by XREAL_1: 19;

 (k ! ) <= ((n |^ k) / (n choose k)) by A7, Lm4;

 hence thesis by INT_1:def 6, A19;

 end;

 theorem :: HILB10_4:18



 Th18: for x,y be Nat holds y = (x ! ) iff ex n,y1,y2,y3 be Nat st y1 = ((2 * x) |^ (x + 1)) & y2 = (n |^ x) & y3 = (n choose x) & n > y1 & y = [\(y2 / y3)/]

 proof

 let x,y be Nat;

 thus y = (x ! ) implies ex n,y1,y2,y3 be Nat st y1 = ((2 * x) |^ (x + 1)) & y2 = (n |^ x) & y3 = (n choose x) & n > y1 & y = [\(y2 / y3)/]

 proof

 assume

 A1: y = (x ! );

 per cases ;

 suppose

 A2: x = 0 ;

 take n = 1, y1 = 0 , y2 = 1, y3 = 1;

 thus y1 = ((2 * x) |^ (x + 1)) & y2 = (n |^ x) & y3 = (n choose x) & n > y1 by A2, NEWTON: 19;

 thus thesis by INT_1: 25, NEWTON: 12, A2, A1;

 end;

 suppose

 A3: x > 0 ;

 take n = (((2 * x) |^ (x + 1)) + 1), y1 = ((2 * x) |^ (x + 1));

 take y2 = (n |^ x), y3 = (n choose x);

 n > y1 by NAT_1: 13;

 hence thesis by A1, A3, Th17;

 end;

 end;

 given n,y1,y2,y3 be Nat such that

 A4: y1 = ((2 * x) |^ (x + 1)) & y2 = (n |^ x) & y3 = (n choose x) & n > y1 and

 A5: y = [\(y2 / y3)/];

 per cases ;

 suppose

 A6: x = 0 ;

 then y1 = 0 & y2 = 1 & y3 = 1 by A4, NEWTON: 4, NEWTON: 19;

 hence thesis by NEWTON: 12, A6, A5, INT_1: 25;

 end;

 suppose x > 0 ;

 hence thesis by A4, A5, Th17;

 end;

 end;

 begin

 reserve x,y,x1,u,w for Nat;

 theorem :: HILB10_4:19



 Th19: for x1,w,u be Nat st ((x1 * w),1) are_congruent_mod u holds for x be Nat holds (( Product (1 + (x1 * ( idseq x)))),(((x1 |^ x) * (x ! )) * ((w + x) choose x))) are_congruent_mod u

 proof

 let x1,w,u be Nat such that

 A1: ((x1 * w),1) are_congruent_mod u;

 consider b be Integer such that

 A2: (u * b) = ((x1 * w) - 1) by A1, INT_1:def 5;

 defpred P[ Nat] means (( Product (1 + (x1 * ( idseq $1)))),(((x1 |^ $1) * ($1 ! )) * ((w + $1) choose $1))) are_congruent_mod u;

 (x1 |^ 0 ) = 1 & ( 0 ! ) = 1 & ((w + 0 ) choose 0 ) = 1 by NEWTON: 4, NEWTON: 12, NEWTON: 19;

 then

 A3: P[ 0 ] by RVSUM_1: 94, INT_1: 11;



 A4: P[n] implies P[(n + 1)]

 proof

 set n1 = (n + 1);

 set P = ( Product (1 + (x1 * ( idseq n))));

 set L = (((x1 |^ n) * (n ! )) * ((w + n) choose n));

 assume P[n];

 then

 consider a be Integer such that

 A5: (u * a) = (P - L) by INT_1:def 5;



 A6: (1 + (x1 * <*n1*>)) = (1 + <*(x1 * n1)*>) by RVSUM_1: 47

 .= <*(1 + (x1 * n1))*> by BASEL_1: 2;

 ( idseq n1) = (( idseq n) ^ <*(n + 1)*>) by FINSEQ_2: 51;

 then (x1 * ( idseq n1)) = ((x1 * ( idseq n)) ^ (x1 * <*(n + 1)*>)) by NEWTON04: 43;

 then

 A7: (1 + (x1 * ( idseq n1))) = ((1 + (x1 * ( idseq n))) ^ (1 + (x1 * <*(n + 1)*>))) by BASEL_1: 3;

 (w + n) >= n & ((w + n) - n) = w by NAT_1: 11;

 then ((w + n) choose n) = (((w + n) ! ) / ((n ! ) * (w ! ))) by NEWTON:def 3;



 then

 A8: ((n ! ) * ((w + n) choose n)) = (((n ! ) * ((w + n) ! )) / ((n ! ) * (w ! ))) by XCMPLX_1: 74

 .= (((w + n) ! ) / (w ! )) by XCMPLX_1: 91;

 (w + n1) >= n1 & ((w + n1) - n1) = w by NAT_1: 11;

 then ((w + n1) choose n1) = (((w + n1) ! ) / ((n1 ! ) * (w ! ))) by NEWTON:def 3;



 then

 A9: ((n1 ! ) * ((w + n1) choose n1)) = (((n1 ! ) * ((w + n1) ! )) / ((n1 ! ) * (w ! ))) by XCMPLX_1: 74

 .= ((((w + n) + 1) ! ) / (w ! )) by XCMPLX_1: 91

 .= ((((w + n) ! ) * ((w + n) + 1)) / (w ! )) by NEWTON: 15

 .= (((w + n) + 1) * (((w + n) ! ) / (w ! ))) by XCMPLX_1: 74

 .= (((w + n1) * (n ! )) * ((w + n) choose n)) by A8;

 (x1 |^ n1) = ((x1 |^ n) * x1) by NEWTON: 6;



 then (((x1 |^ n1) * (n1 ! )) * ((w + n1) choose n1)) = (((x1 |^ n) * x1) * ((n1 ! ) * ((w + n1) choose n1)))

 .= (((x1 |^ n) * x1) * ((((w + n) + 1) * (n ! )) * ((w + n) choose n))) by A9

 .= (((w + n1) * x1) * L);



 then (( Product (1 + (x1 * ( idseq n1)))) - (((x1 |^ n1) * (n1 ! )) * ((w + n1) choose n1))) = ((P * (1 + (x1 * n1))) - ((x1 * (w + n1)) * L)) by A7, A6, RVSUM_1: 96

 .= (((P * (1 + (x1 * n1))) - ((x1 * w) * L)) - ((x1 * n1) * L))

 .= (((P * (1 + (x1 * n1))) - (((u * b) + 1) * L)) - ((x1 * n1) * L)) by A2

 .= (((P - L) * (1 + (x1 * n1))) - (((u * b) * 1) * L))

 .= (((u * a) * (1 + (x1 * n1))) - ((u * b) * L)) by A5

 .= (u * ((a * (1 + (x1 * n1))) - (b * L)));

 hence thesis by INT_1:def 5;

 end;

 P[n] from NAT_1:sch 2( A3, A4);

 hence thesis;

 end;

 theorem :: HILB10_4:20



 Th20: for x,y,x1 be Nat st x1 >= 1 holds y = ( Product (1 + (x1 * ( idseq x)))) iff ex u,w,y1,y2,y3,y4,y5 be Nat st u > y & ((x1 * w),1) are_congruent_mod u & y1 = (x1 |^ x) & y2 = (x ! ) & y3 = ((w + x) choose x) & (((y1 * y2) * y3),y) are_congruent_mod u & y4 = (1 + (x1 * x)) & y5 = (y4 |^ x) & u > y5

 proof

 let x,y,x1 be Nat;

 assume

 A1: x1 >= 1;

 defpred P[ Nat] means ((1 + (x1 * $1)) |^ $1) >= ( Product (1 + (x1 * ( idseq $1))));



 A2: P[ 0 ] by RVSUM_1: 94;



 A3: P[n] implies P[(n + 1)]

 proof

 assume

 A4: P[n];

 set n1 = (n + 1);



 A5: (1 + (x1 * <*n1*>)) = (1 + <*(x1 * n1)*>) by RVSUM_1: 47

 .= <*(1 + (x1 * n1))*> by BASEL_1: 2;

 ( idseq n1) = (( idseq n) ^ <*(n + 1)*>) by FINSEQ_2: 51;

 then (x1 * ( idseq n1)) = ((x1 * ( idseq n)) ^ (x1 * <*(n + 1)*>)) by NEWTON04: 43;

 then (1 + (x1 * ( idseq n1))) = ((1 + (x1 * ( idseq n))) ^ (1 + (x1 * <*(n + 1)*>))) by BASEL_1: 3;

 then

 A6: ( Product (1 + (x1 * ( idseq n1)))) = (( Product (1 + (x1 * ( idseq n)))) * (1 + (x1 * n1))) by A5, RVSUM_1: 96;

 (x1 * n) <= (x1 * n1) by NAT_1: 11, XREAL_1: 64;

 then (1 + (x1 * n)) <= (1 + (x1 * n1)) by XREAL_1: 7;

 then ((1 + (x1 * n)) |^ n) <= ((1 + (x1 * n1)) |^ n) by PREPOWER: 9;

 then (((1 + (x1 * n)) |^ n) * (1 + (x1 * n1))) <= (((1 + (x1 * n1)) |^ n) * (1 + (x1 * n1))) by XREAL_1: 64;

 then

 A7: (((1 + (x1 * n)) |^ n) * (1 + (x1 * n1))) <= ((1 + (x1 * n1)) |^ n1) by NEWTON: 6;

 (( Product (1 + (x1 * ( idseq n)))) * (1 + (x1 * n1))) <= (((1 + (x1 * n)) |^ n) * (1 + (x1 * n1))) by A4, XREAL_1: 64;

 hence thesis by A7, A6, XXREAL_0: 2;

 end;



 A8: P[n] from NAT_1:sch 2( A2, A3);

 thus y = ( Product (1 + (x1 * ( idseq x)))) implies ex u,w,y1,y2,y3,y4,y5 be Nat st u > y & ((x1 * w),1) are_congruent_mod u & y1 = (x1 |^ x) & y2 = (x ! ) & y3 = ((w + x) choose x) & (((y1 * y2) * y3),y) are_congruent_mod u & y4 = (1 + (x1 * x)) & y5 = (y4 |^ x) & u > y5

 proof

 assume

 A9: y = ( Product (1 + (x1 * ( idseq x))));

 set u = ((x1 * ((1 + (x1 * x)) |^ x)) + 1);

 (u gcd x1) = (1 gcd x1) by EULER_1: 16

 .= 1 by WSIERP_1: 8;

 then

 consider w be Nat such that

 A10: (((x1 * w) - 1) mod u) = 0 by INT_4: 16, INT_2:def 3;

 take u, w, y1 = (x1 |^ x), y2 = (x ! ), y3 = ((w + x) choose x), y4 = (1 + (x1 * x)), y5 = (y4 |^ x);



 A11: ((x1 * w) - 1) = (((((x1 * w) - 1) div u) * u) + 0 ) by A10, INT_1: 59;

 then (y,(((x1 |^ x) * (x ! )) * ((w + x) choose x))) are_congruent_mod u by A9, Th19, INT_1:def 5;

 then

 consider e be Integer such that

 A12: ((((x1 |^ x) * (x ! )) * ((w + x) choose x)) - y) = (u * e) by INT_1:def 5, INT_1: 14;

 ((1 + (x1 * x)) |^ x) >= ( Product (1 + (x1 * ( idseq x)))) by A8;

 then (x1 * ((1 + (x1 * x)) |^ x)) >= (1 * ( Product (1 + (x1 * ( idseq x))))) by A1, XREAL_1: 66;

 hence u > y by A9, NAT_1: 13;

 thus ((x1 * w),1) are_congruent_mod u by A11, INT_1:def 5;



 A13: ((x1 * ((1 + (x1 * x)) |^ x)) + 1) > ((x1 * ((1 + (x1 * x)) |^ x)) + 0 ) by XREAL_1: 6;

 (x1 * ((1 + (x1 * x)) |^ x)) >= (1 * ((1 + (x1 * x)) |^ x)) by A1, XREAL_1: 66;

 hence thesis by A12, INT_1:def 5, A13, XXREAL_0: 2;

 end;

 given u,w,y1,y2,y3,y4,y5 be Nat such that

 A14: u > y & ((x1 * w),1) are_congruent_mod u and

 A15: y1 = (x1 |^ x) & y2 = (x ! ) & y3 = ((w + x) choose x) and

 A16: (((y1 * y2) * y3),y) are_congruent_mod u and

 A17: y4 = (1 + (x1 * x)) & y5 = (y4 |^ x) & u > y5;

 set U = (((x1 |^ x) * (x ! )) * ((w + x) choose x));

 (( Product (1 + (x1 * ( idseq x)))),U) are_congruent_mod u by A14, Th19;

 then

 A18: (U,( Product (1 + (x1 * ( idseq x))))) are_congruent_mod u by INT_1: 14;



 A19: ( Product (1 + (x1 * ( idseq x)))) is Nat by TARSKI: 1;

 ( Product (1 + (x1 * ( idseq x)))) <= ((1 + (x1 * x)) |^ x) by A8;

 then ( Product (1 + (x1 * ( idseq x)))) c2)) = (n |-> (c1 + c2))

 proof



 A1: ( len (c1 + (n |-> c2))) = ( len (n |-> c2)) = n = ( len (n |-> (c1 + c2))) by CARD_1:def 7;

 now

 let i such that

 A2: 1 <= i <= n;



 A3: i in ( dom (c1 + (n |-> c2))) by A2, A1, FINSEQ_3: 25;



 A4: i in ( Seg n) by A2;



 hence ((n |-> (c1 + c2)) . i) = (c1 + c2) by FINSEQ_2: 57

 .= (c1 + ((n |-> c2) . i)) by A4, FINSEQ_2: 57

 .= ((c1 + (n |-> c2)) . i) by A3, VALUED_1:def 2;

 end;

 hence thesis by FINSEQ_1: 14, A1;

 end;

 theorem :: HILB10_4:22

 for x,y,x1 be Nat st x1 = 0 holds y = ( Product (1 + (x1 * ( idseq x)))) iff y = 1

 proof

 let x,y,x1 be Nat such that

 A1: x1 = 0 ;



 A2: ( len ( idseq x)) = x;

 ( rng ( idseq x)) c= REAL ;

 then ( idseq x) is FinSequence of REAL by FINSEQ_1:def 4;

 then ( idseq x) is Element of (x -tuples_on REAL ) by A2, FINSEQ_2: 92;

 then (x1 * ( idseq x)) = (x |-> 0 ) by A1, RVSUM_1: 53;

 then (1 + (x1 * ( idseq x))) = (x |-> (1 + 0 )) by Th21;

 hence thesis by RVSUM_1: 102;

 end;

 theorem :: HILB10_4:23



 Th23: n >= k implies ( Product ((n + 1) + ( - ( idseq k)))) = ((k ! ) * (n choose k))

 proof

 defpred P[ Nat] means $1 <= n implies ( Product ((n + 1) + ( - ( idseq $1)))) = (($1 ! ) * (n choose $1));



 A1: P[ 0 ] by RVSUM_1: 94, NEWTON: 12, NEWTON: 19;



 A2: P[i] implies P[(i + 1)]

 proof

 set i1 = (i + 1);

 assume

 A3: P[i] & i1 <= n;



 A4: (( - 1) * <*i1*>) = ( - <*i1*>)

 .= <*( - i1)*> by RVSUM_1: 20;

 ( - ( idseq i1)) = (( - 1) * (( idseq i) ^ <*i1*>)) by FINSEQ_2: 51

 .= (( - ( idseq i)) ^ <*( - i1)*>) by A4, NEWTON04: 43;



 then ((n + 1) + ( - ( idseq i1))) = (((n + 1) + ( - ( idseq i))) ^ ((n + 1) + <*( - i1)*>)) by BASEL_1: 3

 .= (((n + 1) + ( - ( idseq i))) ^ <*((n + 1) + ( - i1))*>) by BASEL_1: 2;

 then

 A5: ( Product ((n + 1) + ( - ( idseq i1)))) = (( Product ((n + 1) + ( - ( idseq i)))) * ((n + 1) + ( - i1))) by RVSUM_1: 96;

 reconsider l = (n - i1) as Element of NAT by A3, NAT_1: 21;



 A6: i <= n & (n - i) = (l + 1) by NAT_1: 13, A3;

 (n choose i1) = ((n ! ) / ((i1 ! ) * (l ! ))) by A3, NEWTON:def 3;



 then ((i1 ! ) * (n choose i1)) = (((i1 ! ) * (n ! )) / ((i1 ! ) * (l ! ))) by XCMPLX_1: 74

 .= ((n ! ) / (l ! )) by XCMPLX_1: 91

 .= (((n ! ) * (l + 1)) / ((l ! ) * (l + 1))) by XCMPLX_1: 91

 .= (((n ! ) * (l + 1)) / ((l + 1) ! )) by NEWTON: 15

 .= ((((n ! ) * (l + 1)) * (i ! )) / (((l + 1) ! ) * (i ! ))) by XCMPLX_1: 91

 .= ((((l + 1) * (i ! )) * (n ! )) / (((l + 1) ! ) * (i ! )))

 .= (((l + 1) * (i ! )) * ((n ! ) / (((l + 1) ! ) * (i ! )))) by XCMPLX_1: 74

 .= ((((n + 1) + ( - i1)) * (i ! )) * (n choose i)) by NEWTON:def 3, A6;

 hence thesis by NAT_1: 13, A3, A5;

 end;

 P[i] from NAT_1:sch 2( A1, A2);

 hence thesis;

 end;

 theorem :: HILB10_4:24

 for y,x1,x2 be Nat holds y = ( Product ((x2 + 1) + ( - ( idseq x1)))) & x2 > x1 iff y = ((x1 ! ) * (x2 choose x1)) & x2 > x1 by Th23;

 begin

 reserve n,m,k for Nat,

p,q for n -element XFinSequence of NAT ,

i1,i2,i3,i4,i5,i6 for Element of n,

a,b,d,f for Integer;

 theorem :: HILB10_4:25



 Th25: for a,b be Nat, i1, i2, i3 holds { p : (p . i1) = (((a * (p . i2)) + b) * (p . i3)) } is diophantine Subset of (n -xtuples_of NAT )

 proof

 let a,b be Nat;

 deffunc F1( Nat, Nat, Nat) = ((a * $1) + b);



 A1: for n, i1, i2, i3, i4 holds { p : F1(.,.,.) = (p . i4) } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 15;

 defpred P1[ Nat, Nat, natural object, Nat, Nat, Nat] means (1 * $1) = ((1 * $3) * $2);



 A2: for n, i1, i2, i3, i4, i5, i6 holds { p : P1[(p . i1), (p . i2), (p . i3), (p . i4), (p . i5), (p . i6)] } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 9;



 A3: for n, i1, i2, i3, i4, i5 holds { p : P1[(p . i1), (p . i2), F1(.,.,.), (p . i3), (p . i4), (p . i5)] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 4( A2, A1);

 let i1, i2, i3;

 defpred Q1[ XFinSequence of NAT ] means P1[($1 . i1), ($1 . i3), ((a * ($1 . i2)) + b), ($1 . i3), ($1 . i3), ($1 . i3)];

 defpred Q2[ XFinSequence of NAT ] means ($1 . i1) = (((a * ($1 . i2)) + b) * ($1 . i3));



 A4: for p holds Q1[p] iff Q2[p];

 { p : Q1[p] } = { q : Q2[q] } from HILB10_3:sch 2( A4);

 hence thesis by A3;

 end;

 theorem :: HILB10_4:26

 for a, i1, i2, i3 holds { p : (p . i1) = ((a * (p . i2)) * (p . i3)) } is diophantine Subset of (n -xtuples_of NAT )

 proof

 let a, i1, i2, i3;

 defpred Q1[ XFinSequence of NAT ] means (1 * ($1 . i1)) = ((a * ($1 . i2)) * ($1 . i3));

 defpred Q2[ XFinSequence of NAT ] means ($1 . i1) = ((a * ($1 . i2)) * ($1 . i3));



 A1: for p holds Q1[p] iff Q2[p];

 { p : Q1[p] } = { q : Q2[q] } from HILB10_3:sch 2( A1);

 hence thesis by HILB10_3: 9;

 end;

 theorem :: HILB10_4:27

 for A be diophantine Subset of (n -xtuples_of NAT ) holds for k,nk be Nat st (k + nk) = n holds { (p /^ nk) : p in A } is diophantine Subset of (k -xtuples_of NAT )

 proof

 let A be diophantine Subset of (n -xtuples_of NAT );

 let k,nk be Nat such that

 A1: (k + nk) = n;

 consider nA be Nat, pA be INT -valued Polynomial of (n + nA), F_Real such that

 A2: for s be object holds s in A iff ex x be n -element XFinSequence of NAT , y be nA -element XFinSequence of NAT st s = x & ( eval (pA,( @ (x ^ y)))) = 0 by HILB10_2:def 6;

 ( dom ( id (n + nA))) = (n + nA);

 then

 reconsider I = ( id (n + nA)) as XFinSequence by AFINSQ_1: 5;

 set I1 = (I | nk), I2 = ((I | n) /^ nk), I3 = (I /^ n);

 ( Segm nk) c= ( Segm n) by NAT_1: 39, NAT_1: 11, A1;

 then

 A3: ((I | n) | nk) = I1 by RELAT_1: 74;

 then

 A4: I = ((I | n) ^ I3) & (I | n) = (I1 ^ I2);

 then

 A5: ( rng (I | n)) misses ( rng I3) by HILB10_2: 1;



 A6: ( len I) = (n + nA);



 A7: n <= (n + nA) by NAT_1: 11;



 A8: ( len I3) = ((n + nA) -' n) = ((n + nA) - n) & ( len (I | n)) = n by A6, AFINSQ_2:def 2, AFINSQ_1: 54, NAT_1: 11;



 A9: ( len I2) = (n -' nk) = (n - nk) & ( len I1) = nk by A1, NAT_1: 11, A8, AFINSQ_2:def 2, AFINSQ_1: 54, A3;



 A10: ( len ((I2 ^ I1) ^ I3)) = (( len (I2 ^ I1)) + ( len I3)) & ( len (I2 ^ I1)) = (( len I2) + ( len I1)) by AFINSQ_1: 17;



 A11: ( rng I1) misses ( rng I2) by A4, HILB10_2: 1;



 A12: (( rng (I | n)) \/ ( rng I3)) = ( rng I) by A4, AFINSQ_1: 26;



 A13: (( rng I1) \/ ( rng I2)) = ( rng (I | n)) & ( rng (I2 ^ I1)) = (( rng I2) \/ ( rng I1)) by A4, AFINSQ_1: 26;

 then ( rng ((I2 ^ I1) ^ I3)) = (n + nA) by A12, AFINSQ_1: 26;

 then

 reconsider J = ((I2 ^ I1) ^ I3) as Function of (n + nA), (n + nA) by A10, A8, A9, FUNCT_2: 1;



 A14: J is onto by A13, A12, AFINSQ_1: 26;



 A15: (I2 ^ I1) is one-to-one by A11, CARD_FIN: 52;

 J is one-to-one by A13, A5, A15, CARD_FIN: 52;

 then

 reconsider J as Permutation of (n + nA) by A14;



 A16: J = ((J " ) " ) by FUNCT_1: 43;

 set h = (pA permuted_by (J " ));

 reconsider H = h as Polynomial of (k + (nk + nA)), F_Real by A1;

 ( rng h) = ( rng pA) c= INT by HILB10_2: 26, RELAT_1:def 19;

 then

 reconsider H as INT -valued Polynomial of (k + (nk + nA)), F_Real by RELAT_1:def 19;

 set Y = { (p /^ nk) : p in A };

 Y c= (k -xtuples_of NAT )

 proof

 let y be object;

 assume y in Y;

 then

 consider p such that

 A17: y = (p /^ nk) & p in A;

 ( len p) = n by CARD_1:def 7;

 then (p /^ nk) is k -element by A1, A9, AFINSQ_2:def 2;

 hence thesis by A17, HILB10_2:def 5;

 end;

 then

 reconsider Y as Subset of (k -xtuples_of NAT );

 for s be object holds s in Y iff ex x be k -element XFinSequence of NAT , y be (nk + nA) -element XFinSequence of NAT st s = x & ( eval (H,( @ (x ^ y)))) = 0

 proof

 let s be object;

 thus s in Y implies ex x be k -element XFinSequence of NAT , y be (nk + nA) -element XFinSequence of NAT st s = x & ( eval (H,( @ (x ^ y)))) = 0

 proof

 assume s in Y;

 then

 consider w be n -element XFinSequence of NAT such that

 A18: s = (w /^ nk) & w in A;

 consider x be n -element XFinSequence of NAT , y be nA -element XFinSequence of NAT such that

 A19: w = x & ( eval (pA,( @ (x ^ y)))) = 0 by A2, A18;



 A20: ( eval (pA,( @ (x ^ y)))) = ( eval (h,(( @ (x ^ y)) * ((J " ) " )))) by HILB10_2: 25;



 A21: ( len x) = n & ( len y) = nA by CARD_1:def 7;

 then

 A22: ( len (x /^ nk)) = k by A1, A9, AFINSQ_2:def 2;

 (x /^ nk) is k -element by A21, A1, A9, AFINSQ_2:def 2;

 then

 reconsider S = (x /^ nk) as k -element XFinSequence of NAT ;



 A23: ( len (x | nk)) = nk by CARD_1:def 7, A1;

 reconsider XnkY = ((x | nk) ^ y) as (nk + nA) -element XFinSequence of NAT by A1;



 A26: ( len (S ^ XnkY)) = (n + nA) by A1, CARD_1:def 7;



 A27: ( dom (( @ (x ^ y)) * J)) = (n + nA) by FUNCT_2:def 1;

 ((x | nk) ^ (x /^ nk)) = x;

 then

 A28: (x ^ y) = ((x | nk) ^ (S ^ y)) by AFINSQ_1: 27;

 for i be object st i in ( dom (S ^ XnkY)) holds ((( @ (x ^ y)) * J) . i) = ((S ^ XnkY) . i)

 proof

 let j be object;

 assume

 A29: j in ( dom (S ^ XnkY));

 then

 reconsider j as Nat;



 A30: j in ( dom J) & ((( @ (x ^ y)) * J) . j) = (( @ (x ^ y)) . (J . j)) by A29, A26, A27, FUNCT_1: 11, FUNCT_1: 12;

 per cases by A30, AFINSQ_1: 20;

 suppose

 A31: j in ( dom (I2 ^ I1));

 then

 A32: (J . j) = ((I2 ^ I1) . j) by AFINSQ_1:def 3;

 per cases by A31, AFINSQ_1: 20;

 suppose

 A33: j in ( dom I2);

 then

 A34: ((I2 ^ I1) . j) = (I2 . j) & (I2 . j) = ((I | n) . (nk + j)) & j < k by A9, A1, AFINSQ_2:def 2, AFINSQ_1: 66, AFINSQ_1:def 3;



 A35: (nk + j) in n by A1, A33, A9, AFINSQ_1: 66, HILB10_3: 3;

 then

 A36: ((I | n) . (nk + j)) = (I . (nk + j)) by FUNCT_1: 49;



 A37: ( dom S) c= ( dom (S ^ y)) by AFINSQ_1: 21;



 A38: ( len S) = k = ( len I2) by CARD_1:def 7, A1, A9;

 ( Segm n) = n;

 then (nk + j) < (n + nA) by NAT_1: 44, A35, A7, XXREAL_0: 2;

 then (nk + j) in ( Segm (n + nA)) by NAT_1: 44;



 then ((( @ (x ^ y)) * J) . j) = (( @ (x ^ y)) . (nk + j)) by FUNCT_1: 17, A32, A30, A36, A34

 .= ((x ^ y) . (nk + j)) by HILB10_2:def 1

 .= ((S ^ y) . j) by A23, A37, A22, A33, A1, A9, A28, AFINSQ_1:def 3

 .= (S . j) by A22, A33, A1, A9, AFINSQ_1:def 3

 .= ((S ^ XnkY) . j) by A33, A38, AFINSQ_1:def 3;

 hence thesis;

 end;

 suppose ex k st k in ( dom I1) & j = (( len I2) + k);

 then

 consider w such that

 A39: w in ( dom I1) & j = (( len I2) + w);



 A40: ((I2 ^ I1) . j) = (I1 . w) & (I1 . w) = (I . w) & w < nk by A39, A9, AFINSQ_1: 66, AFINSQ_1:def 3, FUNCT_1: 49;



 A41: ( dom (x | nk)) c= ( dom ((x | nk) ^ y)) by AFINSQ_1: 21;

 nk <= (nk + (k + nA)) by NAT_1: 11;

 then w < (n + nA) by A1, A39, A9, AFINSQ_1: 66, XXREAL_0: 2;

 then

 A42: w in ( Segm (n + nA)) by NAT_1: 44;

 (J . j) = w by A42, A40, A32, FUNCT_1: 17;



 then ((( @ (x ^ y)) * J) . j) = (((x | nk) ^ (S ^ y)) . w) by A30, A28, HILB10_2:def 1

 .= ((x | nk) . w) by AFINSQ_1:def 3, A39, A23, A9

 .= (((x | nk) ^ y) . w) by A39, A23, A9, AFINSQ_1:def 3

 .= ((S ^ XnkY) . j) by A22, A39, A1, A9, A41, A23, AFINSQ_1:def 3;

 hence thesis;

 end;

 end;

 suppose ex n st n in ( dom I3) & j = (( len (I2 ^ I1)) + n);

 then

 consider w such that

 A43: w in ( dom I3) & j = (( len (I2 ^ I1)) + w);



 A44: ( len (S ^ (x | nk))) = n by CARD_1:def 7, A1;

 (J . j) = (I3 . w) by A43, AFINSQ_1:def 3

 .= (I . j) by A9, A10, A43, AFINSQ_2:def 2

 .= j by A29, A26, FUNCT_1: 17;



 then ((( @ (x ^ y)) * J) . j) = ((x ^ y) . j) by A30, HILB10_2:def 1

 .= (y . w) by A9, A10, A43, A8, A21, AFINSQ_1:def 3

 .= (((S ^ (x | nk)) ^ y) . j) by A44, A9, A10, A43, A8, A21, AFINSQ_1:def 3

 .= ((S ^ XnkY) . j) by AFINSQ_1: 27;

 hence thesis;

 end;

 end;

 then (( @ (x ^ y)) * J) = (S ^ XnkY) by CARD_1:def 7, A1, A27, FUNCT_1: 2;

 then (( @ (x ^ y)) * J) = ( @ (S ^ XnkY)) by HILB10_2:def 1;

 hence thesis by A19, A18, A20, A16;

 end;

 given S be k -element XFinSequence of NAT , XnkY be (nk + nA) -element XFinSequence of NAT such that

 A45: s = S & ( eval (H,( @ (S ^ XnkY)))) = 0 ;

 set Xnk = (XnkY | nk);

 set y = (XnkY /^ nk);

 set X = (Xnk ^ S);



 A46: ( len S) = k & ( len XnkY) = (nk + nA) & (nk + nA) >= nk by NAT_1: 11, CARD_1:def 7;

 then

 A47: ( len Xnk) = nk & ( len y) = ((nk + nA) -' nk) = ((nk + nA) - nk) by AFINSQ_1: 54, AFINSQ_2:def 2;

 reconsider y as nA -element XFinSequence of NAT by A47, CARD_1:def 7;

 reconsider X as n -element XFinSequence of NAT by A1;



 A48: (X | nk) = Xnk by A47, AFINSQ_1: 57;

 (Xnk ^ S) = ((X | nk) ^ (X /^ nk));

 then

 A49: (X /^ nk) = S by A48, AFINSQ_1: 28;



 A50: XnkY = (Xnk ^ y);



 A51: ( len X) = n & ( len y) = nA by CARD_1:def 7;



 A52: ( len (X | nk)) = nk by A47, AFINSQ_1: 57;



 A53: ( len (S ^ XnkY)) = (n + nA) by CARD_1:def 7, A1;



 A54: ( dom (( @ (X ^ y)) * J)) = (n + nA) by FUNCT_2:def 1;



 A55: (X ^ y) = ((X | nk) ^ (S ^ y)) by A48, AFINSQ_1: 27;

 for i be object st i in ( dom (S ^ XnkY)) holds ((( @ (X ^ y)) * J) . i) = ((S ^ XnkY) . i)

 proof

 let j be object;

 assume

 A56: j in ( dom (S ^ XnkY));

 then

 reconsider j as Nat;



 A57: j in ( dom J) & ((( @ (X ^ y)) * J) . j) = (( @ (X ^ y)) . (J . j)) by A56, A53, A54, FUNCT_1: 11, FUNCT_1: 12;

 per cases by A57, AFINSQ_1: 20;

 suppose

 A58: j in ( dom (I2 ^ I1));

 then

 A59: (J . j) = ((I2 ^ I1) . j) by AFINSQ_1:def 3;

 per cases by A58, AFINSQ_1: 20;

 suppose

 A60: j in ( dom I2);

 then

 A61: ((I2 ^ I1) . j) = (I2 . j) & (I2 . j) = ((I | n) . (nk + j)) & j < k by A9, A1, AFINSQ_2:def 2, AFINSQ_1: 66, AFINSQ_1:def 3;

 then

 A63: ((I | n) . (nk + j)) = (I . (nk + j)) by A1, HILB10_3: 3, FUNCT_1: 49;



 A62: (nk + j) in n by A60, A1, HILB10_3: 3, A9, AFINSQ_1: 66;



 A64: ( dom S) c= ( dom (S ^ y)) by AFINSQ_1: 21;



 A65: ( len S) = k = ( len I2) by CARD_1:def 7, A1, A9;

 ( Segm n) = n;

 then (nk + j) < (n + nA) by NAT_1: 44, A62, A7, XXREAL_0: 2;

 then (nk + j) in ( Segm (n + nA)) by NAT_1: 44;

 then (I . (nk + j)) = (nk + j) by FUNCT_1: 17;



 then ((( @ (X ^ y)) * J) . j) = (((X | nk) ^ (S ^ y)) . (nk + j)) by A55, HILB10_2:def 1, A59, A57, A63, A61

 .= ((S ^ y) . j) by A52, A64, A60, A1, A46, A9, AFINSQ_1:def 3

 .= (S . j) by A60, A1, A46, A9, AFINSQ_1:def 3

 .= ((S ^ XnkY) . j) by A60, A65, AFINSQ_1:def 3;

 hence thesis;

 end;

 suppose ex k st k in ( dom I1) & j = (( len I2) + k);

 then

 consider w such that

 A66: w in ( dom I1) & j = (( len I2) + w);



 A67: ((I2 ^ I1) . j) = (I1 . w) & (I1 . w) = (I . w) & w < nk by A66, A9, AFINSQ_1: 66, AFINSQ_1:def 3, FUNCT_1: 49;



 A68: ( dom (X | nk)) c= ( dom ((X | nk) ^ y)) by AFINSQ_1: 21;

 nk <= (nk + (k + nA)) by NAT_1: 11;

 then w < (n + nA) by A1, A66, A9, AFINSQ_1: 66, XXREAL_0: 2;

 then

 A69: w in ( Segm (n + nA)) by NAT_1: 44;

 (J . j) = w by A59, A69, FUNCT_1: 17, A67;



 then ((( @ (X ^ y)) * J) . j) = ((X ^ y) . w) by HILB10_2:def 1, A57

 .= ((X | nk) . w) by AFINSQ_1:def 3, A66, A52, A9, A55

 .= (((X | nk) ^ y) . w) by A66, A52, A9, AFINSQ_1:def 3

 .= ((S ^ XnkY) . j) by A48, A46, A1, A9, A68, A47, A66, AFINSQ_1:def 3;

 hence thesis;

 end;

 end;

 suppose ex n st n in ( dom I3) & j = (( len (I2 ^ I1)) + n);

 then

 consider w such that

 A70: w in ( dom I3) & j = (( len (I2 ^ I1)) + w);



 A71: ( len (S ^ (X | nk))) = n by A1, CARD_1:def 7;

 (J . j) = (I3 . w) by A70, AFINSQ_1:def 3

 .= (I . j) by A9, A10, A70, AFINSQ_2:def 2

 .= j by A56, A53, FUNCT_1: 17;



 then ((( @ (X ^ y)) * J) . j) = ((X ^ y) . j) by HILB10_2:def 1, A57

 .= (y . w) by A9, A10, A70, A8, A51, AFINSQ_1:def 3

 .= (((S ^ (X | nk)) ^ y) . j) by A71, A9, A10, A70, A8, A51, AFINSQ_1:def 3

 .= ((S ^ XnkY) . j) by AFINSQ_1: 27, A48, A50;

 hence thesis;

 end;

 end;

 then (( @ (X ^ y)) * J) = (S ^ XnkY) by CARD_1:def 7, A1, A54, FUNCT_1: 2;

 then (( @ (X ^ y)) * J) = ( @ (S ^ XnkY)) by HILB10_2:def 1;

 then ( eval (H,( @ (S ^ XnkY)))) = ( eval (pA,( @ (X ^ y)))) by A16, HILB10_2: 25;

 then X in A by A2, A45;

 hence s in Y by A49, A45;

 end;

 hence thesis by HILB10_2:def 6;

 end;

 theorem :: HILB10_4:28



 Th28: for a,b be Integer, c be Nat, i1, i2, i3 holds { p : (a * (p . i1)) = [\((b * (p . i2)) / (c * (p . i3)))/] & ((c * (p . i3)) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT )

 proof

 let a,b be Integer, c be Nat;

 let i1, i2, i3;

 deffunc F2( Nat, Nat, Nat) = ((c * $3) + (((a * c) * $1) * $3));



 A1: for n, i1, i2, i3, i4, d holds { p : F2(.,.,.) = (d * (p . i4)) } is diophantine Subset of (n -xtuples_of NAT )

 proof

 let n, i1, i2, i3, i4, d;

 defpred P1[ Nat, Nat, Integer] means (d * $1) = (((c * $2) + $3) + 0 );



 A2: for n, i1, i2, i3, f holds { p : P1[(p . i1), (p . i2), (f * (p . i3))] } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 11;

 deffunc F1( Nat, Nat, Nat) = (((a * c) * $1) * $3);



 A3: for n, i1, i2, i3, i4, f holds { p : F1(.,.,.) = (f * (p . i4)) } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 9;



 A4: for n, i1, i2, i3, i4, i5 holds { p : P1[(p . i1), (p . i2), F1(.,.,.)] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 5( A2, A3);

 defpred R1[ XFinSequence of NAT ] means F2(.,.,.) = (d * ($1 . i4));

 defpred R2[ XFinSequence of NAT ] means P1[($1 . i4), ($1 . i3), F1(.,.,.)];



 A5: for p holds R1[p] iff R2[p];

 { p : R1[p] } = { q : R2[q] } from HILB10_3:sch 2( A5);

 hence thesis by A4;

 end;

 defpred P2[ Nat, Nat, Integer] means ((b * $1) + 0 ) < $3;



 A6: for n, i1, i2, i3, d holds { p : P2[(p . i1), (p . i2), (d * (p . i3))] } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 7;



 A7: for n, i1, i2, i3, i4, i5 holds { p : P2[(p . i1), (p . i2), F2(.,.,.)] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 5( A6, A1);

 defpred P3[ Nat, Nat, Integer] means (b * $1) >= ($3 + 0 );



 A8: for n, i1, i2, i3, d holds { p : P3[(p . i1), (p . i2), (d * (p . i3))] } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 8;

 deffunc F3( Nat, Nat, Nat) = (((a * c) * $1) * $3);



 A9: for n, i1, i2, i3, i4, d holds { p : F3(.,.,.) = (d * (p . i4)) } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 9;



 A10: for n, i1, i2, i3, i4, i5 holds { p : P3[(p . i1), (p . i2), F3(.,.,.)] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 5( A8, A9);

 defpred Q1[ XFinSequence of NAT ] means P2[($1 . i2), ($1 . i2), F2(.,.,.)];

 defpred Q2[ XFinSequence of NAT ] means P3[($1 . i2), ($1 . i2), F3(.,.,.)];

 defpred Q12[ XFinSequence of NAT ] means Q1[$1] & Q2[$1];

 defpred Q3[ XFinSequence of NAT ] means (c * ($1 . i3)) <> (( 0 * ($1 . i3)) + 0 );

 defpred Q123[ XFinSequence of NAT ] means Q12[$1] & Q3[$1];

 defpred T[ XFinSequence of NAT ] means (a * ($1 . i1)) = [\((b * ($1 . i2)) / (c * ($1 . i3)))/] & (c * ($1 . i3)) <> 0 ;



 A11: { p : Q1[p] } is diophantine Subset of (n -xtuples_of NAT ) by A7;



 A12: { p : Q2[p] } is diophantine Subset of (n -xtuples_of NAT ) by A10;

 { p : Q1[p] & Q2[p] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 3( A11, A12);

 then

 A13: { p : Q12[p] } is diophantine Subset of (n -xtuples_of NAT );



 A14: { p : Q3[p] } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 16;



 A15: { p : Q12[p] & Q3[p] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 3( A13, A14);



 A16: for p holds T[p] iff Q123[p]

 proof

 let p;

 thus T[p] implies Q123[p]

 proof

 assume

 A17: T[p];

 then

 A18: ((a * (p . i1)) * (c * (p . i3))) <= (b * (p . i2)) by XREAL_1: 83, INT_1:def 6;

 (((b * (p . i2)) / (c * (p . i3))) * (c * (p . i3))) = (((c * (p . i3)) / (c * (p . i3))) * (b * (p . i2))) by XCMPLX_1: 75

 .= (1 * (b * (p . i2))) by A17, XCMPLX_1: 60;

 then

 A19: ((((b * (p . i2)) / (c * (p . i3))) - 1) * (c * (p . i3))) = ((b * (p . i2)) - (c * (p . i3)));

 (((b * (p . i2)) / (c * (p . i3))) - 1) < (a * (p . i1)) by A17, INT_1:def 6;

 then ((((b * (p . i2)) / (c * (p . i3))) - 1) * (c * (p . i3))) < ((a * (p . i1)) * (c * (p . i3))) by A17, XREAL_1: 68;

 hence thesis by A18, A19, XREAL_1: 19;

 end;

 assume

 A20: Q123[p];

 then

 A21: ((a * (p . i1)) * (c * (p . i3))) > ((b * (p . i2)) - (c * (p . i3))) by XREAL_1: 19;

 (((b * (p . i2)) / (c * (p . i3))) * (c * (p . i3))) = (((c * (p . i3)) / (c * (p . i3))) * (b * (p . i2))) by XCMPLX_1: 75

 .= (1 * (b * (p . i2))) by A20, XCMPLX_1: 60;

 then ((((b * (p . i2)) / (c * (p . i3))) - 1) * (c * (p . i3))) = ((b * (p . i2)) - (c * (p . i3)));

 then

 A22: (a * (p . i1)) > (((b * (p . i2)) / (c * (p . i3))) - 1) by A21, XREAL_1: 64;

 ((a * (p . i1)) * (c * (p . i3))) <= (b * (p . i2)) by A20;

 then (a * (p . i1)) <= ((b * (p . i2)) / (c * (p . i3))) by A20, XREAL_1: 77;

 hence thesis by A20, A22, INT_1:def 6;

 end;

 { p : T[p] } = { q : Q123[q] } from HILB10_3:sch 2( A16);

 hence thesis by A15;

 end;

 theorem :: HILB10_4:29



 Th29: for i1, i2, i3 st n <> 0 holds { p : (p . i1) >= (p . i3) & (p . i2) = ((p . i1) choose (p . i3)) } is diophantine Subset of (n -xtuples_of NAT )

 proof

 let i1, i2, i3;

 set n6 = (n + 6);

 defpred R[ XFinSequence of NAT ] means ($1 . i1) >= ($1 . i3) & ($1 . i2) = (($1 . i1) choose ($1 . i3));

 set RR = { p : R[p] };

 assume

 A1: n <> 0 ;

 n = (n + 0 );

 then

 reconsider X = i1, Y = i2, Z = i3, U = n, V = (n + 1), Y1 = (n + 2), Y2 = (n + 3), Y3 = (n + 4), U1 = (n + 5) as Element of (n + 6) by HILB10_3: 2, HILB10_3: 3;

 defpred P1[ XFinSequence of NAT ] means ($1 . Y1) = (($1 . X) |^ ($1 . Z));



 A2: { p where p be n6 -element XFinSequence of NAT : P1[p] } is diophantine Subset of (n6 -xtuples_of NAT ) by HILB10_3: 24;

 defpred P2[ XFinSequence of NAT ] means ($1 . Y2) = (($1 . U1) |^ ($1 . X));



 A3: { p where p be n6 -element XFinSequence of NAT : P2[p] } is diophantine Subset of (n6 -xtuples_of NAT ) by HILB10_3: 24;

 defpred P3[ XFinSequence of NAT ] means ($1 . Y3) = (($1 . U) |^ ($1 . Z));



 A4: { p where p be n6 -element XFinSequence of NAT : P3[p] } is diophantine Subset of (n6 -xtuples_of NAT ) by HILB10_3: 24;

 defpred P4[ XFinSequence of NAT ] means (1 * ($1 . U)) > ((1 * ($1 . Y1)) + 0 );



 A5: { p where p be n6 -element XFinSequence of NAT : P4[p] } is diophantine Subset of (n6 -xtuples_of NAT ) by HILB10_3: 7;

 defpred P5[ XFinSequence of NAT ] means (1 * ($1 . V)) = [\((1 * ($1 . Y2)) / (1 * ($1 . Y3)))/] & (1 * ($1 . Y3)) <> 0 ;



 A6: { p where p be n6 -element XFinSequence of NAT : P5[p] } is diophantine Subset of (n6 -xtuples_of NAT ) by Th28;

 defpred P6[ XFinSequence of NAT ] means ((1 * ($1 . Y)),(1 * ($1 . V))) are_congruent_mod (1 * ($1 . U));



 A7: { p where p be n6 -element XFinSequence of NAT : P6[p] } is diophantine Subset of (n6 -xtuples_of NAT ) by HILB10_3: 21;

 defpred P7[ XFinSequence of NAT ] means (1 * ($1 . U)) > ((1 * ($1 . Y)) + 0 );



 A8: { p where p be n6 -element XFinSequence of NAT : P7[p] } is diophantine Subset of (n6 -xtuples_of NAT ) by HILB10_3: 7;

 defpred P8[ XFinSequence of NAT ] means (1 * ($1 . X)) >= ((1 * ($1 . Z)) + 0 );



 A9: { p where p be n6 -element XFinSequence of NAT : P8[p] } is diophantine Subset of (n6 -xtuples_of NAT ) by HILB10_3: 8;

 defpred P9[ XFinSequence of NAT ] means (1 * ($1 . U1)) = ((1 * ($1 . U)) + 1);



 A10: { p where p be n6 -element XFinSequence of NAT : P9[p] } is diophantine Subset of (n6 -xtuples_of NAT ) by HILB10_3: 6;

 defpred P12[ XFinSequence of NAT ] means P1[$1] & P2[$1];



 A11: { p where p be n6 -element XFinSequence of NAT : P12[p] } is diophantine Subset of (n6 -xtuples_of NAT ) from HILB10_3:sch 3( A2, A3);

 defpred P123[ XFinSequence of NAT ] means P12[$1] & P3[$1];



 A12: { p where p be n6 -element XFinSequence of NAT : P123[p] } is diophantine Subset of (n6 -xtuples_of NAT ) from HILB10_3:sch 3( A11, A4);

 defpred P1234[ XFinSequence of NAT ] means P123[$1] & P4[$1];



 A13: { p where p be n6 -element XFinSequence of NAT : P1234[p] } is diophantine Subset of (n6 -xtuples_of NAT ) from HILB10_3:sch 3( A12, A5);

 defpred P12345[ XFinSequence of NAT ] means P1234[$1] & P5[$1];



 A14: { p where p be n6 -element XFinSequence of NAT : P12345[p] } is diophantine Subset of (n6 -xtuples_of NAT ) from HILB10_3:sch 3( A13, A6);

 defpred P123456[ XFinSequence of NAT ] means P12345[$1] & P6[$1];



 A15: { p where p be n6 -element XFinSequence of NAT : P123456[p] } is diophantine Subset of (n6 -xtuples_of NAT ) from HILB10_3:sch 3( A14, A7);

 defpred P1234567[ XFinSequence of NAT ] means P123456[$1] & P7[$1];



 A16: { p where p be n6 -element XFinSequence of NAT : P1234567[p] } is diophantine Subset of (n6 -xtuples_of NAT ) from HILB10_3:sch 3( A15, A8);

 defpred P12345678[ XFinSequence of NAT ] means P1234567[$1] & P8[$1];



 A17: { p where p be n6 -element XFinSequence of NAT : P12345678[p] } is diophantine Subset of (n6 -xtuples_of NAT ) from HILB10_3:sch 3( A16, A9);

 defpred P123456789[ XFinSequence of NAT ] means P12345678[$1] & P9[$1];

 set PP = { p where p be n6 -element XFinSequence of NAT : P123456789[p] };



 A18: PP is diophantine Subset of (n6 -xtuples_of NAT ) from HILB10_3:sch 3( A17, A10);

 reconsider PPn = { (p | n) where p be n6 -element XFinSequence of NAT : p in PP } as diophantine Subset of (n -xtuples_of NAT ) by NAT_1: 11, HILB10_3: 5, A18;



 A19: PPn c= RR

 proof

 let x be object;

 assume x in PPn;

 then

 consider p be n6 -element XFinSequence of NAT such that

 A20: x = (p | n) & p in PP;

 ex q be n6 -element XFinSequence of NAT st q = p & P123456789[q] by A20;

 then

 A21: (p . X) >= (p . Z) & (p . Y) = ((p . X) choose (p . Z)) by Th16;

 ((p | n) . X) = (p . i1) & ((p | n) . Y) = (p . i2) & ((p | n) . Z) = (p . i3) by A1, HILB10_3: 4;

 hence thesis by A21, A20;

 end;

 RR c= PPn

 proof

 let x be object;

 assume x in RR;

 then

 consider p such that

 A22: x = p & R[p];

 consider u,v,y1,y2,y3 be Nat such that

 A23: y1 = ((p . i1) |^ (p . i3)) & y2 = ((u + 1) |^ (p . i1)) & y3 = (u |^ (p . i3)) & u > y1 & v = [\(y2 / y3)/] & ((p . i2),v) are_congruent_mod u & (p . i2) = (p . i3) by A22, Th16;

 reconsider u1 = (u + 1) as Element of NAT ;

 reconsider u, v, y1, y2, y3 as Element of NAT by ORDINAL1:def 12;

 set Y = ((((( <%u%> ^ <%v%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%u1%>);

 set PY = (p ^ Y);



 A24: ( len p) = n & ( len Y) = 6 by CARD_1:def 7;



 A25: (PY | n) = p by A24, AFINSQ_1: 57;



 A26: (PY . i3) = ((PY | n) . i3) by A1, HILB10_3: 4

 .= (p . i3) by A24, AFINSQ_1: 57;

 0 in ( dom Y) by AFINSQ_1: 66;



 then

 A27: (PY . (n + 0 )) = (Y . 0 ) by A24, AFINSQ_1:def 3

 .= u by AFINSQ_1: 47;

 1 in ( dom Y) by A24, AFINSQ_1: 66;



 then

 A28: (PY . (n + 1)) = (Y . 1) by A24, AFINSQ_1:def 3

 .= v by AFINSQ_1: 47;

 2 in ( dom Y) by A24, AFINSQ_1: 66;



 then

 A29: (PY . (n + 2)) = (Y . 2) by A24, AFINSQ_1:def 3

 .= y1 by AFINSQ_1: 47;

 3 in ( dom Y) by A24, AFINSQ_1: 66;



 then

 A30: (PY . (n + 3)) = (Y . 3) by A24, AFINSQ_1:def 3

 .= y2 by AFINSQ_1: 47;

 4 in ( dom Y) by A24, AFINSQ_1: 66;



 then

 A31: (PY . (n + 4)) = (Y . 4) by A24, AFINSQ_1:def 3

 .= y3 by AFINSQ_1: 47;

 5 in ( dom Y) by A24, AFINSQ_1: 66;



 then

 A32: (PY . (n + 5)) = (Y . 5) by A24, AFINSQ_1:def 3

 .= u1 by AFINSQ_1: 47;

 P123456789[PY] by A23, A25, A1, HILB10_3: 4, A26, A27, A28, A29, A30, A31, A32;

 then PY in PP;

 hence thesis by A25, A22;

 end;

 hence thesis by A19, XBOOLE_0:def 10;

 end;

 theorem :: HILB10_4:30



 Th30: for i1, i2, i3 holds { p : (p . i1) >= (p . i3) & (p . i2) = ((p . i1) choose (p . i3)) } is diophantine Subset of (n -xtuples_of NAT )

 proof

 let i1, i2, i3;

 set n6 = (n + 6);

 defpred R[ XFinSequence of NAT ] means ($1 . i1) >= ($1 . i3) & ($1 . i2) = (($1 . i1) choose ($1 . i3));

 set RR = { p : R[p] };

 per cases ;

 suppose

 A1: n = 0 ;

 RR c= (n -xtuples_of NAT )

 proof

 let x be object;

 assume x in RR;

 then ex p be n -element XFinSequence of NAT st x = p & R[p];

 hence thesis by HILB10_2:def 5;

 end;

 hence thesis by A1;

 end;

 suppose n <> 0 ;

 hence thesis by Th29;

 end;

 end;

 theorem :: HILB10_4:31



 Th31: for i1, i2 st n <> 0 holds { p : (p . i1) = ((p . i2) ! ) } is diophantine Subset of (n -xtuples_of NAT )

 proof

 let i1, i2;

 set n6 = (n + 6);

 defpred R[ XFinSequence of NAT ] means ($1 . i1) = (($1 . i2) ! );

 set RR = { p : R[p] };

 assume

 A1: n <> 0 ;

 n = (n + 0 );

 then

 reconsider Y = i1, X = i2, N = n, Y1 = (n + 1), Y2 = (n + 2), Y3 = (n + 3), X1 = (n + 4), X2 = (n + 5) as Element of (n + 6) by HILB10_3: 2, HILB10_3: 3;

 defpred P1[ XFinSequence of NAT ] means ($1 . Y1) = (($1 . X2) |^ ($1 . X1));



 A2: { p where p be n6 -element XFinSequence of NAT : P1[p] } is diophantine Subset of (n6 -xtuples_of NAT ) by HILB10_3: 24;

 defpred P2[ XFinSequence of NAT ] means ($1 . Y2) = (($1 . N) |^ ($1 . X));



 A3: { p where p be n6 -element XFinSequence of NAT : P2[p] } is diophantine Subset of (n6 -xtuples_of NAT ) by HILB10_3: 24;

 defpred P3[ XFinSequence of NAT ] means ($1 . N) >= ($1 . X) & ($1 . Y3) = (($1 . N) choose ($1 . X));



 A4: { p where p be n6 -element XFinSequence of NAT : P3[p] } is diophantine Subset of (n6 -xtuples_of NAT ) by Th30;

 defpred P4[ XFinSequence of NAT ] means (1 * ($1 . Y)) = [\((1 * ($1 . Y2)) / (1 * ($1 . Y3)))/] & (1 * ($1 . Y3)) <> 0 ;



 A5: { p where p be n6 -element XFinSequence of NAT : P4[p] } is diophantine Subset of (n6 -xtuples_of NAT ) by Th28;

 defpred P5[ XFinSequence of NAT ] means (1 * ($1 . X2)) = ((2 * ($1 . X)) + 0 );



 A6: { p where p be n6 -element XFinSequence of NAT : P5[p] } is diophantine Subset of (n6 -xtuples_of NAT ) by HILB10_3: 6;

 defpred P6[ XFinSequence of NAT ] means (1 * ($1 . X1)) = ((1 * ($1 . X)) + 1);



 A7: { p where p be n6 -element XFinSequence of NAT : P6[p] } is diophantine Subset of (n6 -xtuples_of NAT ) by HILB10_3: 6;

 defpred P7[ XFinSequence of NAT ] means (1 * ($1 . N)) > ((1 * ($1 . Y1)) + 0 );



 A8: { p where p be n6 -element XFinSequence of NAT : P7[p] } is diophantine Subset of (n6 -xtuples_of NAT ) by HILB10_3: 7;

 defpred P12[ XFinSequence of NAT ] means P1[$1] & P2[$1];



 A9: { p where p be n6 -element XFinSequence of NAT : P12[p] } is diophantine Subset of (n6 -xtuples_of NAT ) from HILB10_3:sch 3( A2, A3);

 defpred P123[ XFinSequence of NAT ] means P12[$1] & P3[$1];



 A10: { p where p be n6 -element XFinSequence of NAT : P123[p] } is diophantine Subset of (n6 -xtuples_of NAT ) from HILB10_3:sch 3( A9, A4);

 defpred P1234[ XFinSequence of NAT ] means P123[$1] & P4[$1];



 A11: { p where p be n6 -element XFinSequence of NAT : P1234[p] } is diophantine Subset of (n6 -xtuples_of NAT ) from HILB10_3:sch 3( A10, A5);

 defpred P12345[ XFinSequence of NAT ] means P1234[$1] & P5[$1];



 A12: { p where p be n6 -element XFinSequence of NAT : P12345[p] } is diophantine Subset of (n6 -xtuples_of NAT ) from HILB10_3:sch 3( A11, A6);

 defpred P123456[ XFinSequence of NAT ] means P12345[$1] & P6[$1];



 A13: { p where p be n6 -element XFinSequence of NAT : P123456[p] } is diophantine Subset of (n6 -xtuples_of NAT ) from HILB10_3:sch 3( A12, A7);

 defpred P1234567[ XFinSequence of NAT ] means P123456[$1] & P7[$1];

 set PP = { p where p be n6 -element XFinSequence of NAT : P1234567[p] };



 A14: PP is diophantine Subset of (n6 -xtuples_of NAT ) from HILB10_3:sch 3( A13, A8);

 reconsider PPn = { (p | n) where p be n6 -element XFinSequence of NAT : p in PP } as diophantine Subset of (n -xtuples_of NAT ) by NAT_1: 11, HILB10_3: 5, A14;



 A15: PPn c= RR

 proof

 let x be object;

 assume x in PPn;

 then

 consider p be n6 -element XFinSequence of NAT such that

 A16: x = (p | n) & p in PP;

 ex q be n6 -element XFinSequence of NAT st q = p & P1234567[q] by A16;

 then

 A17: (p . Y) = ((p . X) ! ) by Th18;

 ((p | n) . X) = (p . i2) & ((p | n) . Y) = (p . i1) by A1, HILB10_3: 4;

 hence thesis by A17, A16;

 end;

 RR c= PPn

 proof

 let x be object;

 assume x in RR;

 then

 consider p such that

 A18: x = p & R[p];

 consider N,y1,y2,y3 be Nat such that

 A19: y1 = ((2 * (p . i2)) |^ ((p . i2) + 1)) & y2 = (N |^ (p . i2)) & y3 = (N choose (p . i2)) & N > y1 & (p . i1) = [\(y2 / y3)/] by Th18, A18;



 A20: (p . i2) <> 0 implies N >= (p . i2)

 proof

 assume (p . i2) <> 0 ;

 then

 A21: (2 * (p . i2)) >= 1 by NAT_1: 14;

 ((p . i2) + 1) >= 1 by NAT_1: 11;

 then

 A22: ((2 * (p . i2)) |^ ((p . i2) + 1)) >= ((2 * (p . i2)) |^ 1) by A21, PREPOWER: 93;

 N > (2 * (p . i2)) & ((p . i2) + (p . i2)) >= (p . i2) by A22, A19, XXREAL_0: 2, NAT_1: 11;

 hence thesis by XXREAL_0: 2;

 end;

 reconsider x1 = ((p . i2) + 1), x2 = (2 * (p . i2)) as Element of NAT ;

 reconsider N, y1, y2, y3 as Element of NAT by ORDINAL1:def 12;

 set Y = ((((( <%N%> ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%x1%>) ^ <%x2%>);

 set PY = (p ^ Y);



 A23: ( len p) = n & ( len Y) = 6 by CARD_1:def 7;



 A24: (PY | n) = p by A23, AFINSQ_1: 57;

 0 in ( dom Y) by AFINSQ_1: 66;



 then

 A25: (PY . (n + 0 )) = (Y . 0 ) by A23, AFINSQ_1:def 3

 .= N by AFINSQ_1: 47;

 1 in ( dom Y) by A23, AFINSQ_1: 66;



 then

 A26: (PY . (n + 1)) = (Y . 1) by A23, AFINSQ_1:def 3

 .= y1 by AFINSQ_1: 47;

 2 in ( dom Y) by A23, AFINSQ_1: 66;



 then

 A27: (PY . (n + 2)) = (Y . 2) by A23, AFINSQ_1:def 3

 .= y2 by AFINSQ_1: 47;

 3 in ( dom Y) by A23, AFINSQ_1: 66;



 then

 A28: (PY . (n + 3)) = (Y . 3) by A23, AFINSQ_1:def 3

 .= y3 by AFINSQ_1: 47;

 4 in ( dom Y) by A23, AFINSQ_1: 66;



 then

 A29: (PY . (n + 4)) = (Y . 4) by A23, AFINSQ_1:def 3

 .= x1 by AFINSQ_1: 47;

 5 in ( dom Y) by A23, AFINSQ_1: 66;



 then

 A30: (PY . (n + 5)) = (Y . 5) by A23, AFINSQ_1:def 3

 .= x2 by AFINSQ_1: 47;

 P1234567[PY] by A20, A19, CATALAN2: 26, A24, A1, HILB10_3: 4, A25, A26, A27, A28, A29, A30;

 then PY in PP;

 hence thesis by A24, A18;

 end;

 hence thesis by A15, XBOOLE_0:def 10;

 end;

 theorem :: HILB10_4:32



 Th32: for i1, i2 holds { p : (p . i1) = ((p . i2) ! ) } is diophantine Subset of (n -xtuples_of NAT )

 proof

 let i1, i2;

 set n6 = (n + 6);

 defpred R[ XFinSequence of NAT ] means ($1 . i1) = (($1 . i2) ! );

 set RR = { p : R[p] };

 per cases ;

 suppose

 A1: n = 0 ;

 RR c= (n -xtuples_of NAT )

 proof

 let x be object;

 assume x in RR;

 then ex p be n -element XFinSequence of NAT st x = p & R[p];

 hence thesis by HILB10_2:def 5;

 end;

 hence thesis by A1;

 end;

 suppose n <> 0 ;

 hence thesis by Th31;

 end;

 end;

 theorem :: HILB10_4:33

 for n, i1, i2, i3 holds { p : (1 + (((p . i1) + 1) * ((p . i2) ! ))) = (p . i3) } is diophantine Subset of (n -xtuples_of NAT )

 proof

 deffunc F1( Nat, Nat, Nat) = ((1 * $1) + ( - 1));



 A1: for i1, i2, i3, i4, a holds { p : F1(.,.,.) = (a * (p . i4)) } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 6;

 defpred P1[ Nat, Nat, Integer] means ((1 * $1) * $2) = $3;



 A2: for i1, i2, i3, a holds { p : P1[(p . i1), (p . i2), (a * (p . i3))] } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 9;



 A3: for i1, i2, i3, i4, i5 holds { p : P1[(p . i1), (p . i2), F1(.,.,.)] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 5( A2, A1);

 deffunc F2( Nat, Nat, Nat) = ($1 ! );



 A4: for i1, i2, i3, i4 holds { p : F2(.,.,.) = (p . i4) } is diophantine Subset of (n -xtuples_of NAT ) by Th32;

 defpred P2[ Nat, Nat, natural object, Nat, Nat, Nat] means ((1 * $1) * $3) = ((1 * $2) - 1);

 A5:

 now

 let n, i1, i3, i2, i4, i5, i6;

 defpred Q1[ XFinSequence of NAT ] means P1[($1 . i1), ($1 . i2), ((1 * ($1 . i3)) + ( - 1))];

 defpred Q2[ XFinSequence of NAT ] means P2[($1 . i1), ($1 . i3), ($1 . i2), ($1 . i4), ($1 . i5), ($1 . i6)];



 A6: for p holds Q1[p] iff Q2[p];

 { p : Q1[p] } = { q : Q2[q] } from HILB10_3:sch 2( A6);

 hence { p : P2[(p . i1), (p . i3), (p . i2), (p . i4), (p . i5), (p . i6)] } is diophantine Subset of (n -xtuples_of NAT ) by A3;

 end;



 A7: for i1, i2, i3, i4, i5 holds { p : P2[(p . i1), (p . i2), F2(.,.,.), (p . i3), (p . i4), (p . i5)] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 4( A5, A4);

 defpred P3[ Nat, Nat, natural object, Nat, Nat, Nat] means ((1 * $3) * ($1 ! )) = ((1 * $2) - 1);



 A8: for n, i1, i4, i2, i3, i5, i6 holds { p : P3[(p . i1), (p . i4), (p . i2), (p . i3), (p . i5), (p . i6)] } is diophantine Subset of (n -xtuples_of NAT ) by A7;

 deffunc F3( Nat, Nat, Nat) = ((1 * $1) + 1);



 A9: for n holds for i1, i2, i3, i4 holds { p : F3(.,.,.) = (p . i4) } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 15;



 A10: for n holds for i1, i2, i3, i4, i5 holds { p : P3[(p . i1), (p . i2), F3(.,.,.), (p . i3), (p . i4), (p . i5)] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 4( A8, A9);

 let n, i1, i2, i3;

 defpred Q1[ XFinSequence of NAT ] means P3[($1 . i2), ($1 . i3), ((1 * ($1 . i1)) + 1), ($1 . i3), ($1 . i3), ($1 . i3)];

 defpred Q2[ XFinSequence of NAT ] means (1 + ((($1 . i1) + 1) * (($1 . i2) ! ))) = ($1 . i3);



 A11: for p holds Q1[p] iff Q2[p];

 { p : Q1[p] } = { q : Q2[q] } from HILB10_3:sch 2( A11);

 hence thesis by A10;

 end;

 theorem :: HILB10_4:34



 Th34: for i1, i2, i3 st n <> 0 holds { p : (p . i3) = ( Product (1 + ((p . i1) * ( idseq (p . i2))))) & (p . i1) >= 1 } is diophantine Subset of (n -xtuples_of NAT )

 proof

 let i1, i2, i3;

 set n12 = (n + 13);

 defpred R[ XFinSequence of NAT ] means ($1 . i3) = ( Product (1 + (($1 . i1) * ( idseq ($1 . i2))))) & ($1 . i1) >= 1;

 set RR = { p : R[p] };

 assume

 A1: n <> 0 ;

 n = (n + 0 );

 then

 reconsider X1 = i1, X = i2, Y = i3, U = n, W = (n + 1), Y1 = (n + 2), Y2 = (n + 3), Y3 = (n + 4), Y4 = (n + 5), Y5 = (n + 6), X1W = (n + 7), WX = (n + 8), Y1Y2 = (n + 9), Y1Y2Y3 = (n + 10), X1X = (n + 11), ONE = (n + 12) as Element of n12 by HILB10_3: 2, HILB10_3: 3;

 defpred P0[ XFinSequence of NAT ] means (1 * ($1 . X1)) >= (( 0 * ($1 . Y)) + 1);



 A2: { p where p be n12 -element XFinSequence of NAT : P0[p] } is diophantine Subset of (n12 -xtuples_of NAT ) by HILB10_3: 8;

 defpred P1[ XFinSequence of NAT ] means (1 * ($1 . U)) > ((1 * ($1 . Y)) + 0 );



 A3: { p where p be n12 -element XFinSequence of NAT : P1[p] } is diophantine Subset of (n12 -xtuples_of NAT ) by HILB10_3: 7;

 defpred P2[ XFinSequence of NAT ] means (1 * ($1 . X1W)) = ((1 * ($1 . X1)) * ($1 . W));



 A4: { p where p be n12 -element XFinSequence of NAT : P2[p] } is diophantine Subset of (n12 -xtuples_of NAT ) by HILB10_3: 9;

 defpred P3[ XFinSequence of NAT ] means ($1 . ONE) = 1;



 A5: { p where p be n12 -element XFinSequence of NAT : P3[p] } is diophantine Subset of (n12 -xtuples_of NAT ) by HILB10_3: 14;

 defpred P4[ XFinSequence of NAT ] means ((1 * ($1 . X1W)),(1 * ($1 . ONE))) are_congruent_mod (1 * ($1 . U));



 A6: { p where p be n12 -element XFinSequence of NAT : P4[p] } is diophantine Subset of (n12 -xtuples_of NAT ) by HILB10_3: 21;

 defpred P5[ XFinSequence of NAT ] means ($1 . Y1) = (($1 . X1) |^ ($1 . X));



 A7: { p where p be n12 -element XFinSequence of NAT : P5[p] } is diophantine Subset of (n12 -xtuples_of NAT ) by HILB10_3: 24;

 defpred P6[ XFinSequence of NAT ] means ($1 . Y2) = (($1 . X) ! );



 A8: { p where p be n12 -element XFinSequence of NAT : P6[p] } is diophantine Subset of (n12 -xtuples_of NAT ) by Th32;

 defpred P7[ XFinSequence of NAT ] means (1 * ($1 . WX)) = (((1 * ($1 . W)) + (1 * ($1 . X))) + 0 );



 A9: { p where p be n12 -element XFinSequence of NAT : P7[p] } is diophantine Subset of (n12 -xtuples_of NAT ) by HILB10_3: 11;

 defpred P8[ XFinSequence of NAT ] means ($1 . WX) >= ($1 . X) & ($1 . Y3) = (($1 . WX) choose ($1 . X));



 A10: { p where p be n12 -element XFinSequence of NAT : P8[p] } is diophantine Subset of (n12 -xtuples_of NAT ) by Th30;

 defpred P9[ XFinSequence of NAT ] means (1 * ($1 . Y1Y2)) = ((1 * ($1 . Y1)) * ($1 . Y2));



 A11: { p where p be n12 -element XFinSequence of NAT : P9[p] } is diophantine Subset of (n12 -xtuples_of NAT ) by HILB10_3: 9;

 defpred PA[ XFinSequence of NAT ] means (1 * ($1 . Y1Y2Y3)) = ((1 * ($1 . Y1Y2)) * ($1 . Y3));



 A12: { p where p be n12 -element XFinSequence of NAT : PA[p] } is diophantine Subset of (n12 -xtuples_of NAT ) by HILB10_3: 9;

 defpred PB[ XFinSequence of NAT ] means ((1 * ($1 . Y1Y2Y3)),(1 * ($1 . Y))) are_congruent_mod (1 * ($1 . U));



 A13: { p where p be n12 -element XFinSequence of NAT : PB[p] } is diophantine Subset of (n12 -xtuples_of NAT ) by HILB10_3: 21;

 defpred PC[ XFinSequence of NAT ] means (1 * ($1 . X1X)) = ((1 * ($1 . X1)) * ($1 . X));



 A14: { p where p be n12 -element XFinSequence of NAT : PC[p] } is diophantine Subset of (n12 -xtuples_of NAT ) by HILB10_3: 9;

 defpred PD[ XFinSequence of NAT ] means (1 * ($1 . Y4)) = ((1 * ($1 . X1X)) + 1);



 A15: { p where p be n12 -element XFinSequence of NAT : PD[p] } is diophantine Subset of (n12 -xtuples_of NAT ) by HILB10_3: 6;

 defpred PE[ XFinSequence of NAT ] means ($1 . Y5) = (($1 . Y4) |^ ($1 . X));



 A16: { p where p be n12 -element XFinSequence of NAT : PE[p] } is diophantine Subset of (n12 -xtuples_of NAT ) by HILB10_3: 24;

 defpred PF[ XFinSequence of NAT ] means (1 * ($1 . U)) > ((1 * ($1 . Y5)) + 0 );



 A17: { p where p be n12 -element XFinSequence of NAT : PF[p] } is diophantine Subset of (n12 -xtuples_of NAT ) by HILB10_3: 7;

 defpred C1[ XFinSequence of NAT ] means P0[$1] & P1[$1];



 A18: { p where p be n12 -element XFinSequence of NAT : C1[p] } is diophantine Subset of (n12 -xtuples_of NAT ) from HILB10_3:sch 3( A2, A3);

 defpred C2[ XFinSequence of NAT ] means C1[$1] & P2[$1];



 A19: { p where p be n12 -element XFinSequence of NAT : C2[p] } is diophantine Subset of (n12 -xtuples_of NAT ) from HILB10_3:sch 3( A18, A4);

 defpred C3[ XFinSequence of NAT ] means C2[$1] & P3[$1];



 A20: { p where p be n12 -element XFinSequence of NAT : C3[p] } is diophantine Subset of (n12 -xtuples_of NAT ) from HILB10_3:sch 3( A19, A5);

 defpred C4[ XFinSequence of NAT ] means C3[$1] & P4[$1];



 A21: { p where p be n12 -element XFinSequence of NAT : C4[p] } is diophantine Subset of (n12 -xtuples_of NAT ) from HILB10_3:sch 3( A20, A6);

 defpred C5[ XFinSequence of NAT ] means C4[$1] & P5[$1];



 A22: { p where p be n12 -element XFinSequence of NAT : C5[p] } is diophantine Subset of (n12 -xtuples_of NAT ) from HILB10_3:sch 3( A21, A7);

 defpred C6[ XFinSequence of NAT ] means C5[$1] & P6[$1];



 A23: { p where p be n12 -element XFinSequence of NAT : C6[p] } is diophantine Subset of (n12 -xtuples_of NAT ) from HILB10_3:sch 3( A22, A8);

 defpred C7[ XFinSequence of NAT ] means C6[$1] & P7[$1];



 A24: { p where p be n12 -element XFinSequence of NAT : C7[p] } is diophantine Subset of (n12 -xtuples_of NAT ) from HILB10_3:sch 3( A23, A9);

 defpred C8[ XFinSequence of NAT ] means C7[$1] & P8[$1];



 A25: { p where p be n12 -element XFinSequence of NAT : C8[p] } is diophantine Subset of (n12 -xtuples_of NAT ) from HILB10_3:sch 3( A24, A10);

 defpred C9[ XFinSequence of NAT ] means C8[$1] & P9[$1];



 A26: { p where p be n12 -element XFinSequence of NAT : C9[p] } is diophantine Subset of (n12 -xtuples_of NAT ) from HILB10_3:sch 3( A25, A11);

 defpred CA[ XFinSequence of NAT ] means C9[$1] & PA[$1];



 A27: { p where p be n12 -element XFinSequence of NAT : CA[p] } is diophantine Subset of (n12 -xtuples_of NAT ) from HILB10_3:sch 3( A26, A12);

 defpred CB[ XFinSequence of NAT ] means CA[$1] & PB[$1];



 A28: { p where p be n12 -element XFinSequence of NAT : CB[p] } is diophantine Subset of (n12 -xtuples_of NAT ) from HILB10_3:sch 3( A27, A13);

 defpred CC[ XFinSequence of NAT ] means CB[$1] & PC[$1];



 A29: { p where p be n12 -element XFinSequence of NAT : CC[p] } is diophantine Subset of (n12 -xtuples_of NAT ) from HILB10_3:sch 3( A28, A14);

 defpred CD[ XFinSequence of NAT ] means CC[$1] & PD[$1];



 A30: { p where p be n12 -element XFinSequence of NAT : CD[p] } is diophantine Subset of (n12 -xtuples_of NAT ) from HILB10_3:sch 3( A29, A15);

 defpred CE[ XFinSequence of NAT ] means CD[$1] & PE[$1];



 A31: { p where p be n12 -element XFinSequence of NAT : CE[p] } is diophantine Subset of (n12 -xtuples_of NAT ) from HILB10_3:sch 3( A30, A16);

 defpred CF[ XFinSequence of NAT ] means CE[$1] & PF[$1];

 set PP = { p where p be n12 -element XFinSequence of NAT : CF[p] };



 A32: PP is diophantine Subset of (n12 -xtuples_of NAT ) from HILB10_3:sch 3( A31, A17);

 reconsider PPn = { (p | n) where p be n12 -element XFinSequence of NAT : p in PP } as diophantine Subset of (n -xtuples_of NAT ) by NAT_1: 11, HILB10_3: 5, A32;



 A33: PPn c= RR

 proof

 let x be object;

 assume x in PPn;

 then

 consider p be n12 -element XFinSequence of NAT such that

 A34: x = (p | n) & p in PP;

 ex q be n12 -element XFinSequence of NAT st q = p & CF[q] by A34;

 then

 A35: R[p] by Th20;

 ((p | n) . X1) = (p . i1) & ((p | n) . X) = (p . i2) & ((p | n) . Y) = (p . i3) by A1, HILB10_3: 4;

 hence thesis by A35, A34;

 end;

 RR c= PPn

 proof

 let x be object;

 assume x in RR;

 then

 consider p such that

 A36: x = p & R[p];

 consider u,w,y1,y2,y3,y4,y5 be Nat such that

 A37: u > (p . i3) & (((p . i1) * w),1) are_congruent_mod u & y1 = ((p . i1) |^ (p . i2)) & y2 = ((p . i2) ! ) & y3 = ((w + (p . i2)) choose (p . i2)) & (((y1 * y2) * y3),(p . i3)) are_congruent_mod u & y4 = (1 + ((p . i1) * (p . i2))) & y5 = (y4 |^ (p . i2)) & u > y5 by A36, Th20;

 reconsider u, w, n, y1, y2, y3, y4, y5 as Element of NAT by ORDINAL1:def 12;

 reconsider x1w = ((p . i1) * w), wx = (w + (p . i2)), y12 = (y1 * y2), y123 = ((y1 * y2) * y3), x1x = ((p . i1) * (p . i2)), One = 1 as Element of NAT ;

 set Y1 = (((((((( <%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>), Y2 = ((( <%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>);

 set Y = (Y1 ^ Y2);

 set PY = (p ^ Y);

 reconsider PY as XFinSequence of NAT ;



 A38: ( len p) = n & ( len Y) = 13 & ( len Y1) = 9 & ( len Y2) = 4 by CARD_1:def 7;



 A39: (PY | n) = p by A38, AFINSQ_1: 57;



 A40: (PY . i2) = ((PY | n) . i2) by A1, HILB10_3: 4

 .= (p . i2) by A38, AFINSQ_1: 57;

 0 in ( dom Y) by AFINSQ_1: 66;



 then

 A41: (PY . (n + 0 )) = (Y . 0 ) by A38, AFINSQ_1:def 3

 .= (Y1 . 0 ) by A38, AFINSQ_1: 51

 .= u by AFINSQ_1: 50;

 1 in ( dom Y) by A38, AFINSQ_1: 66;



 then

 A42: (PY . (n + 1)) = (Y . 1) by A38, AFINSQ_1:def 3

 .= (Y1 . 1) by A38, AFINSQ_1: 51

 .= w by AFINSQ_1: 50;

 2 in ( dom Y) by A38, AFINSQ_1: 66;



 then

 A43: (PY . (n + 2)) = (Y . 2) by A38, AFINSQ_1:def 3

 .= (Y1 . 2) by A38, AFINSQ_1: 51

 .= y1 by AFINSQ_1: 50;

 3 in ( dom Y) by A38, AFINSQ_1: 66;



 then

 A44: (PY . (n + 3)) = (Y . 3) by A38, AFINSQ_1:def 3

 .= (Y1 . 3) by A38, AFINSQ_1: 51

 .= y2 by AFINSQ_1: 50;

 4 in ( dom Y) by A38, AFINSQ_1: 66;



 then

 A45: (PY . (n + 4)) = (Y . 4) by A38, AFINSQ_1:def 3

 .= (Y1 . 4) by A38, AFINSQ_1: 51

 .= y3 by AFINSQ_1: 50;

 5 in ( dom Y) by A38, AFINSQ_1: 66;



 then

 A46: (PY . (n + 5)) = (Y . 5) by A38, AFINSQ_1:def 3

 .= (Y1 . 5) by A38, AFINSQ_1: 51

 .= y4 by AFINSQ_1: 50;

 6 in ( dom Y) by A38, AFINSQ_1: 66;



 then

 A47: (PY . (n + 6)) = (Y . 6) by A38, AFINSQ_1:def 3

 .= (Y1 . 6) by A38, AFINSQ_1: 51

 .= y5 by AFINSQ_1: 50;

 7 in ( dom Y) by A38, AFINSQ_1: 66;



 then

 A48: (PY . (n + 7)) = (Y . 7) by A38, AFINSQ_1:def 3

 .= (Y1 . 7) by A38, AFINSQ_1: 51

 .= x1w by AFINSQ_1: 50;

 8 in ( dom Y) by A38, AFINSQ_1: 66;



 then

 A49: (PY . (n + 8)) = (Y . 8) by A38, AFINSQ_1:def 3

 .= (Y1 . 8) by A38, AFINSQ_1: 51

 .= wx by AFINSQ_1: 50;



 A50: 9 in ( dom Y) & 0 in ( dom Y2) by A38, AFINSQ_1: 66;



 then

 A51: (PY . (n + 9)) = (Y . (9 + 0 )) by A38, AFINSQ_1:def 3

 .= (Y2 . 0 ) by A38, A50, AFINSQ_1:def 3

 .= y12 by AFINSQ_1: 45;



 A52: 10 in ( dom Y) & 1 in ( dom Y2) by A38, AFINSQ_1: 66;



 then

 A53: (PY . (n + 10)) = (Y . (9 + 1)) by A38, AFINSQ_1:def 3

 .= (Y2 . 1) by A38, A52, AFINSQ_1:def 3

 .= y123 by AFINSQ_1: 45;



 A54: 11 in ( dom Y) & 2 in ( dom Y2) by A38, AFINSQ_1: 66;



 then

 A55: (PY . (n + 11)) = (Y . (9 + 2)) by A38, AFINSQ_1:def 3

 .= (Y2 . 2) by A38, A54, AFINSQ_1:def 3

 .= x1x by AFINSQ_1: 45;



 A56: 12 in ( dom Y) & 3 in ( dom Y2) by A38, AFINSQ_1: 66;



 then

 A57: (PY . (n + 12)) = (Y . (9 + 3)) by A38, AFINSQ_1:def 3

 .= (Y2 . 3) by A38, A56, AFINSQ_1:def 3

 .= One by AFINSQ_1: 45;

 CF[PY] by A36, A37, A39, A1, HILB10_3: 4, A40, A41, A42, A43, A44, A45, A46, A47, A48, A49, A51, A53, A55, A57, NAT_1: 11;

 then PY in PP;

 hence thesis by A39, A36;

 end;

 hence thesis by A33, XBOOLE_0:def 10;

 end;

 theorem :: HILB10_4:35



 Th35: for i1, i2, i3 holds { p : (p . i3) = ( Product (1 + ((p . i1) * ( idseq (p . i2))))) & (p . i1) >= 1 } is diophantine Subset of (n -xtuples_of NAT )

 proof

 let i1, i2, i3;

 set n12 = (n + 13);

 defpred R[ XFinSequence of NAT ] means ($1 . i3) = ( Product (1 + (($1 . i1) * ( idseq ($1 . i2))))) & ($1 . i1) >= 1;

 set RR = { p : R[p] };

 per cases ;

 suppose

 A1: n = 0 ;

 RR c= (n -xtuples_of NAT )

 proof

 let x be object;

 assume x in RR;

 then ex p be n -element XFinSequence of NAT st x = p & R[p];

 hence thesis by HILB10_2:def 5;

 end;

 hence thesis by A1;

 end;

 suppose n <> 0 ;

 hence thesis by Th34;

 end;

 end;

 theorem :: HILB10_4:36

 for n, i1, i2, i3 holds { p : (p . i3) = ( Product (1 + (((p . i1) ! ) * ( idseq (1 + (p . i2)))))) } is diophantine Subset of (n -xtuples_of NAT )

 proof

 deffunc F1( Nat, Nat, Nat) = ($1 ! );



 A1: for i1, i2, i3, i4 holds { p : F1(.,.,.) = (p . i4) } is diophantine Subset of (n -xtuples_of NAT ) by Th32;

 defpred P1[ Nat, Nat, natural object, Nat, Nat, Nat] means $1 = ( Product (1 + ($3 * ( idseq $2)))) & $3 >= 1;



 A2: for i1, i2, i3, i4, i5, i6 holds { p : P1[(p . i1), (p . i2), (p . i3), (p . i4), (p . i5), (p . i6)] } is diophantine Subset of (n -xtuples_of NAT ) by Th35;



 A3: for i1, i2, i3, i4, i5 holds { p : P1[(p . i1), (p . i2), F1(.,.,.), (p . i3), (p . i4), (p . i5)] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 4( A2, A1);

 deffunc F2( Nat, Nat, Nat) = ((1 * $1) + 1);



 A4: for i1, i2, i3, i4 holds { p : F2(.,.,.) = (p . i4) } is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 15;

 defpred P2[ Nat, Nat, natural object, Nat, Nat, Nat] means $1 = ( Product (1 + (($2 ! ) * ( idseq $3)))) & ($2 ! ) >= 1;



 A5: for n, i1, i3, i2, i4, i5, i6 holds { p : P2[(p . i1), (p . i3), (p . i2), (p . i4), (p . i5), (p . i6)] } is diophantine Subset of (n -xtuples_of NAT ) by A3;



 A6: for i1, i2, i3, i4, i5 holds { p : P2[(p . i1), (p . i2), F2(.,.,.), (p . i3), (p . i4), (p . i5)] } is diophantine Subset of (n -xtuples_of NAT ) from HILB10_3:sch 4( A5, A4);

 let n, i1, i2, i3;

 defpred Q1[ XFinSequence of NAT ] means P2[($1 . i3), ($1 . i1), ((1 * ($1 . i2)) + 1), (1 * ($1 . i3)), ($1 . i3), ($1 . i3)];

 defpred Q2[ XFinSequence of NAT ] means ($1 . i3) = ( Product (1 + ((($1 . i1) ! ) * ( idseq (1 + ($1 . i2))))));



 A7: for p holds Q1[p] iff Q2[p] by NAT_1: 14;

 { p : Q1[p] } = { q : Q2[q] } from HILB10_3:sch 2( A7);

 hence thesis by A6;

 end;

 theorem :: HILB10_4:37



 Th37: for i1, i2, i3 st n <> 0 holds { p : (p . i3) = ( Product (((p . i2) + 1) + ( - ( idseq (p . i1))))) & (p . i2) > (p . i1) } is diophantine Subset of (n -xtuples_of NAT )

 proof

 let i1, i2, i3;

 set n2 = (n + 2);

 defpred R[ XFinSequence of NAT ] means ($1 . i3) = ( Product ((($1 . i2) + 1) + ( - ( idseq ($1 . i1))))) & ($1 . i2) > ($1 . i1);

 set RR = { p : R[p] };

 assume

 A1: n <> 0 ;

 n = (n + 0 );

 then

 reconsider Y = i3, X2 = i2, X1 = i1, C = n, F = (n + 1) as Element of n2 by HILB10_3: 2, HILB10_3: 3;

 defpred P1[ XFinSequence of NAT ] means ($1 . X2) >= ($1 . X1) & ($1 . C) = (($1 . X2) choose ($1 . X1));



 A2: { p where p be n2 -element XFinSequence of NAT : P1[p] } is diophantine Subset of (n2 -xtuples_of NAT ) by Th30;

 defpred P2[ XFinSequence of NAT ] means ($1 . F) = (($1 . X1) ! );



 A3: { p where p be n2 -element XFinSequence of NAT : P2[p] } is diophantine Subset of (n2 -xtuples_of NAT ) by Th32;

 defpred P3[ XFinSequence of NAT ] means (1 * ($1 . X2)) > ((1 * ($1 . X1)) + 0 );



 A4: { p where p be n2 -element XFinSequence of NAT : P3[p] } is diophantine Subset of (n2 -xtuples_of NAT ) by HILB10_3: 7;

 defpred P4[ XFinSequence of NAT ] means (1 * ($1 . Y)) = ((1 * ($1 . F)) * ($1 . C));



 A5: { p where p be n2 -element XFinSequence of NAT : P4[p] } is diophantine Subset of (n2 -xtuples_of NAT ) by HILB10_3: 9;

 defpred P12[ XFinSequence of NAT ] means P1[$1] & P2[$1];



 A6: { p where p be n2 -element XFinSequence of NAT : P12[p] } is diophantine Subset of (n2 -xtuples_of NAT ) from HILB10_3:sch 3( A2, A3);

 defpred P123[ XFinSequence of NAT ] means P12[$1] & P3[$1];



 A7: { p where p be n2 -element XFinSequence of NAT : P123[p] } is diophantine Subset of (n2 -xtuples_of NAT ) from HILB10_3:sch 3( A6, A4);

 defpred P1234[ XFinSequence of NAT ] means P123[$1] & P4[$1];

 set PP = { p where p be n2 -element XFinSequence of NAT : P1234[p] };



 A8: PP is diophantine Subset of (n2 -xtuples_of NAT ) from HILB10_3:sch 3( A7, A5);

 reconsider PPn = { (p | n) where p be n2 -element XFinSequence of NAT : p in PP } as diophantine Subset of (n -xtuples_of NAT ) by NAT_1: 11, HILB10_3: 5, A8;



 A9: PPn c= RR

 proof

 let x be object;

 assume x in PPn;

 then

 consider p be n2 -element XFinSequence of NAT such that

 A10: x = (p | n) & p in PP;

 ex q be n2 -element XFinSequence of NAT st q = p & P1234[q] by A10;

 then

 A11: R[p] by Th23;

 ((p | n) . X2) = (p . i2) & ((p | n) . X1) = (p . i1) & ((p | n) . Y) = (p . i3) by A1, HILB10_3: 4;

 hence thesis by A11, A10;

 end;

 RR c= PPn

 proof

 let x be object;

 assume x in RR;

 then

 consider p such that

 A12: x = p & R[p];

 reconsider F = ((p . i1) ! ), C = ((p . i2) choose (p . i1)) as Element of NAT ;

 set Y = <%C, F%>;

 set PY = (p ^ Y);



 A13: ( len p) = n & ( len Y) = 2 by CARD_1:def 7;



 A14: (PY | n) = p by A13, AFINSQ_1: 57;



 A15: (PY . i2) = ((PY | n) . i2) by A1, HILB10_3: 4

 .= (p . i2) by A13, AFINSQ_1: 57;



 A16: (PY . i3) = ((PY | n) . i3) by A1, HILB10_3: 4

 .= (p . i3) by A13, AFINSQ_1: 57;

 0 in ( dom Y) by AFINSQ_1: 66;



 then

 A17: (PY . (n + 0 )) = (Y . 0 ) by A13, AFINSQ_1:def 3

 .= C;

 1 in ( dom Y) by A13, AFINSQ_1: 66;



 then

 A18: (PY . (n + 1)) = (Y . 1) by A13, AFINSQ_1:def 3

 .= F;

 P1234[PY] by A12, A14, A1, HILB10_3: 4, A16, A15, A17, A18, Th23;

 then PY in PP;

 hence thesis by A14, A12;

 end;

 hence thesis by A9, XBOOLE_0:def 10;

 end;

 theorem :: HILB10_4:38

 for i1, i2, i3 holds { p : (p . i3) = ( Product (((p . i2) + 1) + ( - ( idseq (p . i1))))) & (p . i2) > (p . i1) } is diophantine Subset of (n -xtuples_of NAT )

 proof

 let i1, i2, i3;

 set n2 = (n + 2);

 defpred R[ XFinSequence of NAT ] means ($1 . i3) = ( Product ((($1 . i2) + 1) + ( - ( idseq ($1 . i1))))) & ($1 . i2) > ($1 . i1);

 set RR = { p : R[p] };

 per cases ;

 suppose

 A1: n = 0 ;

 RR c= (n -xtuples_of NAT )

 proof

 let x be object;

 assume x in RR;

 then ex p be n -element XFinSequence of NAT st x = p & R[p];

 hence thesis by HILB10_2:def 5;

 end;

 hence thesis by A1;

 end;

 suppose n <> 0 ;

 hence thesis by Th37;

 end;

 end;

 theorem :: HILB10_4:39

 for i, n1, n2, n, i1 holds { p : (p . i1) = ( Product (i + ((p /^ n1) | n2))) } is diophantine Subset of (n -xtuples_of NAT )

 proof

 let i, n1, n2;

 defpred P[ Nat] means for n st ($1 + n1) <= n holds for i1 holds { p : (p . i1) = ( Product (i + ((p /^ n1) | $1))) } is diophantine Subset of (n -xtuples_of NAT );



 A1: P[ 0 ]

 proof

 let n;

 assume ( 0 + n1) <= n;

 let i1;

 defpred Q1[ XFinSequence of NAT ] means ($1 . i1) = ( Product (i + (($1 /^ n1) | 0 )));

 defpred Q2[ XFinSequence of NAT ] means ($1 . i1) = 1;



 A2: for p holds Q1[p] iff Q2[p] by Th4;

 { p : Q1[p] } = { q : Q2[q] } from HILB10_3:sch 2( A2);

 hence thesis by HILB10_3: 14;

 end;



 A3: P[m] implies P[(m + 1)]

 proof

 assume

 A4: P[m];

 let n such that

 A5: ((m + 1) + n1) <= n;

 set m1 = (m + 1), X = (n + 1);

 let i1;

 m < m1 by NAT_1: 13;

 then (n1 + m) < (n1 + m1) 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 < X by NAT_1: 13;

 then n in ( Segm X) by NAT_1: 44;

 then

 reconsider N = n, I1 = i1, N1M = n1m as Element of X by HILB10_3: 2;

 defpred P[ XFinSequence of NAT ] means ($1 . N) = ( Product (i + (($1 /^ n1) | m)));

 defpred Q[ XFinSequence of NAT ] means ($1 . I1) = (((1 * ($1 . N1M)) + i) * ($1 . N));

 (n1 + m) <= X by A6, NAT_1: 13;

 then

 A8: { p where p be X -element XFinSequence of NAT : P[p] } is diophantine Subset of (X -xtuples_of NAT ) by A4;



 A9: { p where p be X -element XFinSequence of NAT : Q[p] } is diophantine Subset of (X -xtuples_of NAT ) by Th25;

 set PQ = { p where p be X -element XFinSequence of NAT : P[p] & Q[p] };



 A10: PQ is diophantine Subset of (X -xtuples_of NAT ) from HILB10_3:sch 3( A8, A9);

 set PQr = { (p | n) where p be X -element XFinSequence of NAT : p in PQ };

 set S = { p : (p . i1) = ( Product (i + ((p /^ n1) | m1))) };



 A11: PQr is diophantine Subset of (n -xtuples_of NAT ) by HILB10_3: 5, A7, A10;



 A12: n1 <= (n1 + m1) <= n by A5, NAT_1: 11;

 then

 A13: (n -' n1) = (n - n1) by XXREAL_0: 2, XREAL_1: 233;



 A14: m1 <= (n - n1) by A5, XREAL_1: 19;

 m < (m + 1) by NAT_1: 13;

 then

 A15: ( Segm m) c= ( Segm m1) & m in ( Segm m1) by NAT_1: 39, NAT_1: 44;



 A16: S c= PQr

 proof

 let y be object;

 assume y in S;

 then

 consider p such that

 A17: y = p & (p . i1) = ( Product (i + ((p /^ n1) | m1)));



 A18: ( len p) = n by CARD_1:def 7;

 then

 A19: ( len (p /^ n1)) >= m1 by A14, A13, AFINSQ_2:def 2;

 then ( len ((p /^ n1) | m1)) = m1 by AFINSQ_1: 54;

 then

 A20: ((p /^ n1) | m1) = ((((p /^ n1) | m1) | m) ^ <%(((p /^ n1) | m1) . m)%>) by AFINSQ_1: 56;

 (((p /^ n1) | m1) | m) = ((p /^ n1) | m) & (((p /^ n1) | m1) . m) = ((p /^ n1) . m) & m in ( dom (p /^ n1)) by A19, AFINSQ_1: 53, RELAT_1: 74, A15;

 then ((p /^ n1) | m1) = (((p /^ n1) | m) ^ <%(p . n1m)%>) by A20, AFINSQ_2:def 2;



 then (i + ((p /^ n1) | m1)) = ((i + ((p /^ n1) | m)) ^ (i + <%(p . n1m)%>)) by Th8

 .= ((i + ((p /^ n1) | m)) ^ <%(i + (p . n1m))%>) by Th9;



 then

 A21: ( Product (i + ((p /^ n1) | m1))) = (( 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 X -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;

 P[pP] & Q[pP] by A23, A25, A21, A18, AFINSQ_1: 36, A17;

 then pP in PQ;

 hence thesis by A17, A24;

 end;

 PQr c= S

 proof

 let y be object;

 assume y in PQr;

 then

 consider pP be X -element XFinSequence of NAT such that

 A26: y = (pP | n) & pP in PQ;



 A27: ex q be X -element XFinSequence of NAT st pP = q & P[q] & Q[q] by A26;



 A28: ( len pP) = X by CARD_1:def 7;



 A29: ( len (pP | n)) = n by CARD_1:def 7;

 set p = (pP | n);



 A30: ( len (p /^ n1)) >= m1 by A14, A13, A29, AFINSQ_2:def 2;

 then ( len ((p /^ n1) | m1)) = m1 by AFINSQ_1: 54;

 then

 A31: ((p /^ n1) | m1) = ((((p /^ n1) | m1) | m) ^ <%(((p /^ n1) | m1) . m)%>) by AFINSQ_1: 56;

 (((p /^ n1) | m1) | m) = ((p /^ n1) | m) & (((p /^ n1) | m1) . m) = ((p /^ n1) . m) & m in ( dom (p /^ n1)) by A30, AFINSQ_1: 53, RELAT_1: 74, A15;

 then ((p /^ n1) | m1) = (((p /^ n1) | m) ^ <%(p . n1m)%>) by A31, AFINSQ_2:def 2;



 then (i + ((p /^ n1) | m1)) = ((i + ((p /^ n1) | m)) ^ (i + <%(p . n1m)%>)) by Th8

 .= ((i + ((p /^ n1) | m)) ^ <%(i + (p . n1m))%>) by Th9;



 then

 A32: ( Product (i + ((p /^ n1) | m1))) = (( Product (i + ((p /^ n1) | m))) * ( Product <%(i + (p . n1m))%>)) by Th7

 .= (( Product (i + ((p /^ n1) | m))) * (i + (p . n1m))) by Th5;

 set P = ( Product (i + ((p /^ n1) | m)));



 A33: pP = (p ^ <%(pP . n)%>) by A28, AFINSQ_1: 56;



 A34: ( len (p /^ n1)) > m by A30, NAT_1: 13;



 A35: ((pP /^ n1) | m) = (((p /^ n1) ^ <%(pP . n)%>) | m) by A33, Th10, A29, A12, XXREAL_0: 2

 .= ((p /^ n1) | m) by AFINSQ_1: 58, A34;

 (pP . I1) = (p . i1) & (pP . N1M) = (p . n1m) by A5, HILB10_3: 4;

 hence thesis by A26, A35, A32, A27;

 end;

 hence thesis by A11, A16, XBOOLE_0:def 10;

 end;



 A36: P[m] from NAT_1:sch 2( A1, A3);

 let n, i1;

 per cases ;

 suppose (n1 + n2) <= n;

 hence thesis by A36;

 end;

 suppose (n1 + n2) > n;

 then

 A37: (n - n1) < n2 by XREAL_1: 19;

 per cases ;

 suppose

 A38: n1 >= n;

 defpred Q1[ XFinSequence of NAT ] means ($1 . i1) = ( Product (i + (($1 /^ n1) | n2)));

 defpred Q2[ XFinSequence of NAT ] means ($1 . i1) = 1;



 A39: for p holds Q1[p] iff Q2[p]

 proof

 let p;

 ( len p) = n by CARD_1:def 7;

 then (p /^ n1) = {} by A38, AFINSQ_2: 6;

 then (i + ((p /^ n1) | n2)) = {} ;

 hence thesis by Th4;

 end;

 { p : Q1[p] } = { q : Q2[q] } from HILB10_3:sch 2( A39);

 hence thesis by HILB10_3: 14;

 end;

 suppose

 A40: n1 < n;

 then

 reconsider N = (n - n1) as Nat by NAT_1: 21;

 defpred Q1[ XFinSequence of NAT ] means ($1 . i1) = ( Product (i + (($1 /^ n1) | n2)));

 defpred Q2[ XFinSequence of NAT ] means ($1 . i1) = ( Product (i + (($1 /^ n1) | N)));



 A41: for p holds Q1[p] iff Q2[p]

 proof

 let p;

 ( len p) = n by CARD_1:def 7;

 then ( len (p /^ n1)) = (n - n1) by A40, AFINSQ_2: 7;

 hence thesis by A37, AFINSQ_1: 52;

 end;



 A42: { p : Q1[p] } = { q : Q2[q] } from HILB10_3:sch 2( A41);

 (n1 + N) = n;

 hence thesis by A42, A36;

 end;

 end;

 end;