let n, D be Nat; :: thesis: ex F being FinSequence of NAT st
( len F = n + 1 & ( for k being Nat st k in dom F holds
F . k = [\((k - 1) * (sqrt D))/] + 1 ) & ( not D is square implies F is one-to-one ) )
deffunc H₁( Nat) -> set = [\(($1 - 1) * (sqrt D))/] + 1;
consider p being FinSequence such that
A1: ( len p = n + 1 & ( for k being Nat st k in dom p holds
p . k = H₁(k) ) ) from FINSEQ_1:sch 2();
rng p c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in NAT )
assume A2: y in rng p ; :: thesis: y in NAT
consider x being object such that
A3: ( x in dom p & p . x = y ) by A2, FUNCT_1:def 3;
reconsider x = x as Nat by A3;
( 1 <= x & x <= n + 1 ) by A3, A1, FINSEQ_3:25;
then A4: 1 - 1 <= x - 1 by XREAL_1:9;
( 0 < D or D = 0 ) ;
then ( 0 < sqrt D or sqrt D = 0 ) by SQUARE_1:25;
then 0 <= H₁(x) by A4, INT_1:29;
then H₁(x) in NAT by INT_1:3;
hence y in NAT by A3, A1; :: thesis: verum

end;

then reconsider p = p as FinSequence of NAT by FINSEQ_1:def 4;
take p ; :: thesis: ( len p = n + 1 & ( for k being Nat st k in dom p holds
p . k = [\((k - 1) * (sqrt D))/] + 1 ) & ( not D is square implies p is one-to-one ) )
thus ( len p = n + 1 & ( for k being Nat st k in dom p holds
p . k = [\((k - 1) * (sqrt D))/] + 1 ) ) by A1; :: thesis: ( not D is square implies p is one-to-one )
assume A5: not D is square ; :: thesis: p is one-to-one
let y1, y2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not y1 in proj1 p or not y2 in proj1 p or not p . y1 = p . y2 or y1 = y2 )
assume A6: ( y1 in dom p & y2 in dom p & p . y1 = p . y2 ) ; :: thesis: y1 = y2
assume A7: y1 <> y2 ; :: thesis: contradiction
reconsider y1 = y1, y2 = y2 as Nat by A6;
A8: ( p . y1 = H₁(y1) & p . y2 = H₁(y2) ) by A6, A1;
not D is trivial by A5;
then A9: ( sqrt D > sqrt 1 & sqrt 1 = 1 ) by NEWTON03:def 1, SQUARE_1:27;

per cases ( y1 < y2 or y1 > y2 ) by A7, XXREAL_0:1;

suppose A10: y1 < y2 ; :: thesis: contradiction

A11: [\((y2 - 1) * (sqrt D))/] + 1 <= ((y1 - 1) * (sqrt D)) + 1 by A6, A8, XREAL_1:6, INT_1:def 6;
(y2 - 1) * (sqrt D) < ((y1 - 1) * (sqrt D)) + 1 by INT_1:29, A11, XXREAL_0:2;
then A12: ((y2 - 1) * (sqrt D)) - ((y1 - 1) * (sqrt D)) <= 1 by XREAL_1:19;
A13: ( (y2 - y1) * ((sqrt D) / (sqrt D)) = ((y2 - y1) * (sqrt D)) / (sqrt D) & ((y2 - y1) * (sqrt D)) / (sqrt D) <= 1 / (sqrt D) ) by A12, A9, XREAL_1:72, XCMPLX_1:74;
A14: ( 1 / (sqrt D) < (sqrt D) / (sqrt D) & (sqrt D) / (sqrt D) = 1 ) by XCMPLX_1:60, A9, XREAL_1:74;
A15: y1 - y1 < y2 - y1 by XREAL_1:9, A10;
y2 - y1 < 1 by XXREAL_0:2, A13, A14;
hence contradiction by NAT_1:14, A15; :: thesis: verum

end;

suppose A16: y1 > y2 ; :: thesis: contradiction

A17: [\((y1 - 1) * (sqrt D))/] + 1 <= ((y2 - 1) * (sqrt D)) + 1 by A6, A8, XREAL_1:6, INT_1:def 6;
(y1 - 1) * (sqrt D) < ((y2 - 1) * (sqrt D)) + 1 by INT_1:29, A17, XXREAL_0:2;
then A18: ((y1 - 1) * (sqrt D)) - ((y2 - 1) * (sqrt D)) <= 1 by XREAL_1:19;
A19: ( (y1 - y2) * ((sqrt D) / (sqrt D)) = ((y1 - y2) * (sqrt D)) / (sqrt D) & ((y1 - y2) * (sqrt D)) / (sqrt D) <= 1 / (sqrt D) ) by A18, A9, XREAL_1:72, XCMPLX_1:74;
A20: ( 1 / (sqrt D) < (sqrt D) / (sqrt D) & (sqrt D) / (sqrt D) = 1 ) by XCMPLX_1:60, A9, XREAL_1:74;
A21: y2 - y2 < y1 - y2 by XREAL_1:9, A16;
y1 - y2 < 1 by XXREAL_0:2, A19, A20;
hence contradiction by NAT_1:14, A21; :: thesis: verum

end;

end;