let a be Real; :: thesis: for t being 1 _greater Nat ex x, y being Integer st
( |.((x * a) - y).| < 1 / t & 0 < x & x <= t )
let t be 1 _greater Nat; :: thesis: ex x, y being Integer st
( |.((x * a) - y).| < 1 / t & 0 < x & x <= t )
consider x1, x2 being object such that
A1: x1 in dom (F_dp1 (t,a)) and
A2: x2 in dom (F_dp1 (t,a)) and
A3: x1 <> x2 and
A4: (F_dp1 (t,a)) . x1 = (F_dp1 (t,a)) . x2 by Th27;
A5: dom (F_dp1 (t,a)) = Seg (len (F_dp1 (t,a))) by FINSEQ_1:def 3
.= Seg (t + 1) by Def4 ;
consider n1 being Nat such that
A6: x1 = n1 and
A7: 1 <= n1 and
A8: n1 <= t + 1 by A1, A5;
reconsider x1 = x1 as Nat by A6;
consider n2 being Nat such that
A9: x2 = n2 and
A10: 1 <= n2 and
A11: n2 <= t + 1 by A2, A5;
reconsider x2 = x2 as Nat by A9;
(F_dp1 (t,a)) . x1 in rng (F_dp1 (t,a)) by A1, FUNCT_1:3;
then (F_dp1 (t,a)) . x1 in Segm t ;
then (F_dp1 (t,a)) . x1 in { i where i is Nat : i < t } by AXIOMS:4;
then consider i being Nat such that
A13: (F_dp1 (t,a)) . x1 = i and
i < t ;
A14: [\((frac ((x1 - 1) * a)) * t)/] = i by Def4, A1, A13;
reconsider r1 = frac ((x1 - 1) * a) as Real ;
(F_dp1 (t,a)) . x2 in rng (F_dp1 (t,a)) by A2, FUNCT_1:3;
then (F_dp1 (t,a)) . x2 in Segm t ;
then (F_dp1 (t,a)) . x2 in { i where i is Nat : i < t } by AXIOMS:4;
then consider i2 being Nat such that
A16: (F_dp1 (t,a)) . x2 = i2 and
i2 < t ;
A17: [\((frac ((x2 - 1) * a)) * t)/] = i2 by Def4, A2, A16;
reconsider r2 = frac ((x2 - 1) * a) as Real ;
i = (F_dp1 (t,a)) . x1 by A13
.= (F_dp1 (t,a)) . x2 by A4
.= i2 by A16 ;
then A18: ( r1 in (Equal_Div_interval t) . i & r2 in (Equal_Div_interval t) . i ) by A14, Lm4, A17;
A19: |.(r1 - r2).| < t " by Lm5, A18;
set m1 = x1 - 1;
set m2 = x2 - 1;
A20: r1 - r2 = (((x1 - 1) * a) - [\((x1 - 1) * a)/]) - (frac ((x2 - 1) * a)) by INT_1:def 8
.= (((x1 - 1) * a) - [\((x1 - 1) * a)/]) - (((x2 - 1) * a) - [\((x2 - 1) * a)/]) by INT_1:def 8
.= (((x1 - 1) - (x2 - 1)) * a) - ([\((x1 - 1) * a)/] - [\((x2 - 1) * a)/]) ;

per cases ( x1 > x2 or x1 < x2 ) by A3, XXREAL_0:1;

suppose A21: x1 > x2 ; :: thesis: ex x, y being Integer st
( |.((x * a) - y).| < 1 / t & 0 < x & x <= t )

set x = (x1 - 1) - (x2 - 1);
set y = [\((x1 - 1) * a)/] - [\((x2 - 1) * a)/];
A24: (x1 - 1) - (x2 - 1) = x1 - x2 ;
A25: (t + 1) - x2 >= x1 - x2 by A6, A8, XREAL_1:13;
(t + 1) - 1 >= (t + 1) - x2 by A9, A10, XREAL_1:10;
then A27: (x1 - 1) - (x2 - 1) <= t by A25, XXREAL_0:2;
A28: 0 < (x1 - 1) - (x2 - 1) by A21, XREAL_1:50, A24;
|.((((x1 - 1) - (x2 - 1)) * a) - ([\((x1 - 1) * a)/] - [\((x2 - 1) * a)/])).| < t " by Lm5, A18, A20;
hence ex x, y being Integer st
( |.((x * a) - y).| < 1 / t & 0 < x & x <= t ) by A27, A28; :: thesis: verum

end;

suppose A29: x1 < x2 ; :: thesis: ex x, y being Integer st
( |.((x * a) - y).| < 1 / t & 0 < x & x <= t )

set x = (x2 - 1) - (x1 - 1);
set y = [\((x2 - 1) * a)/] - [\((x1 - 1) * a)/];
A32: (x2 - 1) - (x1 - 1) = x2 - x1 ;
A33: (t + 1) - x1 >= x2 - x1 by A9, A11, XREAL_1:13;
(t + 1) - 1 >= (t + 1) - x1 by A6, A7, XREAL_1:10;
then A35: (x2 - 1) - (x1 - 1) <= t by A33, XXREAL_0:2;
A36: 0 < (x2 - 1) - (x1 - 1) by A29, XREAL_1:50, A32;
- (r1 - r2) = (((x2 - 1) - (x1 - 1)) * a) - ([\((x2 - 1) * a)/] - [\((x1 - 1) * a)/]) by A20;
then |.((((x2 - 1) - (x1 - 1)) * a) - ([\((x2 - 1) * a)/] - [\((x1 - 1) * a)/])).| < t " by A19, COMPLEX1:52;
hence ex x, y being Integer st
( |.((x * a) - y).| < 1 / t & 0 < x & x <= t ) by A35, A36; :: thesis: verum

end;

end;