let a be Nat; :: thesis:
let k be Integer; :: thesis:
assume that
A1: a <> 0 and
A2: a gcd k = 1 ; :: thesis:
A3: a >= 1 by A1, NAT_1:14;

per cases by A3, XXREAL_0:1;

suppose A4: a = 1 ; :: thesis:

take b = 1; :: thesis:
take e = 1; :: thesis:
thus ( b <> 0 & e <> 0 ) ; :: thesis:
thus ( b <= sqrt a & e <= sqrt a ) by A4; :: thesis:
thus ( a divides (k * b) + e or a divides (k * b) - e ) by A4, INT_2:12; :: thesis:

end;

suppose A5: a > 1 ; :: thesis:

A6: sqrt a > 0 by A1, SQUARE_1:25;
set d = [\(sqrt a)/];
A7: [\(sqrt a)/] <= sqrt a by INT_1:def 6;
sqrt a < a by A5, Lm21;
then A8: [\(sqrt a)/] < a by A7, XXREAL_0:2;
set d1 = [\(sqrt a)/] + 1;
A9: [\(sqrt a)/] > (sqrt a) - 1 by INT_1:def 6;
sqrt a > 1 by A5, SQUARE_1:18, SQUARE_1:27;
then A10: (sqrt a) - 1 > 0 by XREAL_1:50;
then reconsider d = [\(sqrt a)/] as Element of NAT by A9, INT_1:3;
A11: d + 1 >= 1 by Lm1;
then reconsider d1 = [\(sqrt a)/] + 1 as Element of NAT ;
set e1 = d1 ^2 ;
d1 ^2 = d1 * d1 ;
then reconsider e1 = d1 ^2 as Element of NAT ;
A12: (e1 - 1) / d1 = d1 - (1 / d1) by A11, XCMPLX_1:127;
deffunc H₁( Nat) -> set = 1 + (((k * (($1 - 1) div d1)) + (($1 - 1) mod d1)) mod a);
consider fs being FinSequence such that
A13: ( len fs = e1 & ( for b being Nat st b in dom fs holds
fs . b = H₁(b) ) ) from FINSEQ_1:sch 2();
A14: rng fs c= Seg a

proof

let v be object ; :: according to TARSKI:def 3 :: thesis:
assume v in rng fs ; :: thesis:
then consider b being Nat such that
A15: ( b in dom fs & fs . b = v ) by FINSEQ_2:10;
A16: v = 1 + (((k * ((b - 1) div d1)) + ((b - 1) mod d1)) mod a) by A13, A15;
then reconsider v1 = v as Integer ;
A17: 0 <= ((k * ((b - 1) div d1)) + ((b - 1) mod d1)) mod a by NEWTON:64;
then A18: 1 <= v1 by A16, Lm1;
reconsider v1 = v1 as Element of NAT by A16, A17, INT_1:3;
((k * ((b - 1) div d1)) + ((b - 1) mod d1)) mod a < a by A1, NEWTON:65;
then v1 <= a by A16, Lm9;
hence v in Seg a by A18; :: thesis:

end;

sqrt a < d1 by A9, XREAL_1:19;
then (sqrt a) ^2 < e1 by A6, SQUARE_1:16;
then A19: a < e1 by SQUARE_1:def 2;
then A20: Seg a c= Seg e1 by FINSEQ_1:5;
A21: Seg e1 = dom fs by A13, FINSEQ_1:def 3;
then rng fs <> dom fs by A19, A14, FINSEQ_1:5;
then not fs is one-to-one by A21, A14, A20, FINSEQ_4:59, XBOOLE_1:1;
then consider v1, v2 being object such that
A22: v1 in dom fs and
A23: v2 in dom fs and
A24: fs . v1 = fs . v2 and
A25: v1 <> v2 by FUNCT_1:def 4;
reconsider v1 = v1, v2 = v2 as Element of NAT by A22, A23;
set x1 = (v1 - 1) div d1;
set x2 = (v2 - 1) div d1;
set x = ((v1 - 1) div d1) - ((v2 - 1) div d1);
set y1 = (v1 - 1) mod d1;
set y2 = (v2 - 1) mod d1;
set y = ((v1 - 1) mod d1) - ((v2 - 1) mod d1);
A26: (v1 - 1) mod d1 >= 0 by NEWTON:64;
( fs . v1 = 1 + (((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) mod a) & fs . v2 = 1 + (((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) mod a) ) by A13, A22, A23;
then A27: (((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1))) mod a = 0 by A24, Lm19, XCMPLX_1:2;
then A28: a divides ((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) by A1, Lm20;
1 / d1 > 0 by A9, A10, XREAL_1:139;
then A29: (e1 - 1) / d1 < d1 by A12, Lm1;
A30: (v2 - 1) div d1 = [\((v2 - 1) / d1)/] by INT_1:def 9;
then A31: (v2 - 1) div d1 <= (v2 - 1) / d1 by INT_1:def 6;
v2 <= e1 by A13, A23, FINSEQ_3:25;
then v2 - 1 <= e1 - 1 by XREAL_1:9;
then (v2 - 1) / d1 <= (e1 - 1) / d1 by XREAL_1:72;
then (v2 - 1) / d1 < d1 by A29, XXREAL_0:2;
then (v2 - 1) div d1 < d1 by A31, XXREAL_0:2;
then A32: (v2 - 1) div d1 <= d by Lm9;
set d2 = (k * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1));
A33: [\0/] = 0 ;
A34: (v1 - 1) div d1 = [\((v1 - 1) / d1)/] by INT_1:def 9;
then A35: (v1 - 1) div d1 <= (v1 - 1) / d1 by INT_1:def 6;
1 <= v1 by A22, FINSEQ_3:25;
then v1 - 1 >= 0 by XREAL_1:48;
then (v1 - 1) div d1 >= 0 by A34, A33, PRE_FF:9;
then ((v2 - 1) div d1) - ((v1 - 1) div d1) <= d by A32, Lm2;
then A36: - (((v2 - 1) div d1) - ((v1 - 1) div d1)) >= - d by XREAL_1:24;
A37: ( ((v1 - 1) div d1) - ((v2 - 1) div d1) <> 0 or ((v1 - 1) mod d1) - ((v2 - 1) mod d1) <> 0 )

proof

assume ( not ((v1 - 1) div d1) - ((v2 - 1) div d1) <> 0 & not ((v1 - 1) mod d1) - ((v2 - 1) mod d1) <> 0 ) ; :: thesis:
then v1 - 1 = (((v2 - 1) div d1) * d1) + ((v2 - 1) mod d1) by A11, NEWTON:66
.= v2 - 1 by A11, NEWTON:66 ;
hence contradiction by A25; :: thesis:

end;

v1 <= e1 by A13, A22, FINSEQ_3:25;
then v1 - 1 <= e1 - 1 by XREAL_1:9;
then (v1 - 1) / d1 <= (e1 - 1) / d1 by XREAL_1:72;
then (v1 - 1) / d1 < d1 by A29, XXREAL_0:2;
then (v1 - 1) div d1 < d1 by A35, XXREAL_0:2;
then A38: (v1 - 1) div d1 <= d by Lm9;
A39: ((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) = (k * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) ;
(v2 - 1) mod d1 < d1 by A9, A10, NEWTON:65;
then ((v2 - 1) mod d1) - ((v1 - 1) mod d1) < d1 by A26, Lm3;
then ((v2 - 1) mod d1) - ((v1 - 1) mod d1) <= d by Lm9;
then A40: - (((v2 - 1) mod d1) - ((v1 - 1) mod d1)) >= - d by XREAL_1:24;
take b = |.(((v1 - 1) div d1) - ((v2 - 1) div d1)).|; :: thesis:
take e = |.(((v1 - 1) mod d1) - ((v2 - 1) mod d1)).|; :: thesis:
A41: (v2 - 1) mod d1 >= 0 by NEWTON:64;
1 <= v2 by A23, FINSEQ_3:25;
then v2 - 1 >= 0 by XREAL_1:48;
then (v2 - 1) div d1 >= 0 by A30, A33, PRE_FF:9;
then ((v1 - 1) div d1) - ((v2 - 1) div d1) <= d by A38, Lm2;
then A42: |.(((v1 - 1) div d1) - ((v2 - 1) div d1)).| <= d by A36, ABSVALUE:5;
then A43: |.(((v1 - 1) div d1) - ((v2 - 1) div d1)).| < a by A8, XXREAL_0:2;

A44: now :: thesis:

assume A45: ((v1 - 1) mod d1) - ((v2 - 1) mod d1) = 0 ; :: thesis:
then a divides ((v1 - 1) div d1) - ((v2 - 1) div d1) by A1, A2, A27, A39, Lm20, Th29;
then a divides |.(((v1 - 1) div d1) - ((v2 - 1) div d1)).| by Lm17;
then |.(((v1 - 1) div d1) - ((v2 - 1) div d1)).| = 0 by A43, NAT_D:7;
hence contradiction by A37, A45, ABSVALUE:2; :: thesis:

end;

(v1 - 1) mod d1 < d1 by A9, A10, NEWTON:65;
then ((v1 - 1) mod d1) - ((v2 - 1) mod d1) < d1 by A41, Lm3;
then ((v1 - 1) mod d1) - ((v2 - 1) mod d1) <= d by Lm9;
then A46: |.(((v1 - 1) mod d1) - ((v2 - 1) mod d1)).| <= d by A40, ABSVALUE:5;
then A47: |.(((v1 - 1) mod d1) - ((v2 - 1) mod d1)).| < a by A8, XXREAL_0:2;

now :: thesis:

assume A48: ((v1 - 1) div d1) - ((v2 - 1) div d1) = 0 ; :: thesis:
then a divides |.(((v1 - 1) mod d1) - ((v2 - 1) mod d1)).| by A28, Lm17;
then |.(((v1 - 1) mod d1) - ((v2 - 1) mod d1)).| = 0 by A47, NAT_D:7;
hence contradiction by A37, A48, ABSVALUE:2; :: thesis:

end;

hence ( b <> 0 & e <> 0 ) by A44, ABSVALUE:2; :: thesis:
thus b <= sqrt a by A7, A42, XXREAL_0:2; :: thesis:
thus e <= sqrt a by A7, A46, XXREAL_0:2; :: thesis:
A49: ( b = ((v1 - 1) div d1) - ((v2 - 1) div d1) or b = - (((v1 - 1) div d1) - ((v2 - 1) div d1)) ) by ABSVALUE:1;
A50: ( e = ((v1 - 1) mod d1) - ((v2 - 1) mod d1) or e = - (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) ) by ABSVALUE:1;
- ((k * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1))) = (k * (- (((v1 - 1) div d1) - ((v2 - 1) div d1)))) + (- (((v1 - 1) mod d1) - ((v2 - 1) mod d1))) ;
hence ( a divides (k * b) + e or a divides (k * b) - e ) by A28, A49, A50, INT_2:10; :: thesis:

end;