theorem :: LIOUVIL1:36

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