theorem LC4: :: ASYMPT_2:19

for a being non negative Real
for n being Nat st 1 <= n holds
0 < (seq_n^ a) . n