theorem Th31: :: LIOUVIL1:33

for a being NAT -valued Real_Sequence
for b being non zero Nat st b >= 2 & rng a c= b holds
Liouville_seq (a,b) is summable