for p being Real st p >= 1 holds
for rseq being Real_Sequence st ( for n being Nat holds rseq . n = 0 ) holds
( rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 )