theorem :: LIOUVIL1:38

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