let k, n be Nat; :: thesis: ( n > 0 implies (aseq k) . n = 1 - (k / n) )
assume A1: n > 0 ; :: thesis: (aseq k) . n = 1 - (k / n)
thus (aseq k) . n = (n - k) / n by Def1
.= (n / n) - (k / n)
.= 1 - (k / n) by A1, XCMPLX_1:60 ; :: thesis: verum