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