theorem Th13: :: IRRAT_1:13

for k, n being Nat st k < n holds
( 0 < (aseq k) . n & (aseq k) . n <= 1 )