theorem Th12: :: LP_SPACE:12

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