theorem Th35: :: LIOUVIL1:39

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