theorem Th7: :: IRRAT_1:7

for k, n being Nat st n > 0 holds
(aseq k) . n = 1 - (k / n)