theorem Th33: :: LIOUVIL1:35

for a being NAT -valued Real_Sequence
for b being non trivial Nat
for n being Nat holds (Liouville_seq (a,b)) . n >= 0