for a being NAT -valued Real_Sequence
for b, c being Nat st b >= 2 & c >= 1 & rng a c= c & c <= b holds
for i being Nat holds (Liouville_seq (a,b)) . i <= ((c - 1) (#) (powerfact b)) . i