let k, n be Element of NAT ; :: thesis: ( k < n implies ( 0 < (aseq k) . n & (aseq k) . n <= 1 ) )
assume A1: k < n ; :: thesis: ( 0 < (aseq k) . n & (aseq k) . n <= 1 )
A2: (aseq k) . n = (n - k) / n by Def1;
n - k > 0 by A1, XREAL_1:52;
hence (aseq k) . n > 0 by A1, A2, XREAL_1:141; :: thesis: (aseq k) . n <= 1
1 - (k / n) <= 1 - 0 by XREAL_1:8;
hence (aseq k) . n <= 1 by A1, Th8; :: thesis: verum