let k, n be Nat; :: thesis: ( k < n implies ( 0 < (aseq k) . n & (aseq k) . n <= 1 ) )

A1: (aseq k) . n = (n - k) / n by Def1;

assume A2: k < n ; :: thesis: ( 0 < (aseq k) . n & (aseq k) . n <= 1 )

then n - k > 0 by XREAL_1:50;

hence (aseq k) . n > 0 by A2, A1, XREAL_1:139; :: thesis: (aseq k) . n <= 1

1 - (k / n) <= 1 - 0 by XREAL_1:6;

hence (aseq k) . n <= 1 by A2, Th7; :: thesis: verum

A1: (aseq k) . n = (n - k) / n by Def1;

assume A2: k < n ; :: thesis: ( 0 < (aseq k) . n & (aseq k) . n <= 1 )

then n - k > 0 by XREAL_1:50;

hence (aseq k) . n > 0 by A2, A1, XREAL_1:139; :: thesis: (aseq k) . n <= 1

1 - (k / n) <= 1 - 0 by XREAL_1:6;

hence (aseq k) . n <= 1 by A2, Th7; :: thesis: verum