for a being NAT -valued Real_Sequence
for b being non trivial Nat
for n being Nat st a is eventually-non-zero & rng a c= b holds
Sum ((Liouville_seq (a,b)) ^\ (n + 1)) > 0