let p be Real; :: thesis: ( 1 <= p implies 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 )

assume A1: 1 <= p ; :: thesis: 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

A2: 1 / p > 0 by ;
let rseq be Real_Sequence; :: thesis: ( rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 implies for n being Nat holds rseq . n = 0 )
assume that
A3: rseq rto_power p is summable and
A4: (Sum (rseq rto_power p)) to_power (1 / p) = 0 ; :: thesis: for n being Nat holds rseq . n = 0
A5: for i being Nat holds (rseq rto_power p) . i >= 0
proof
let i be Nat; :: thesis: (rseq rto_power p) . i >= 0
(rseq rto_power p) . i = |.(rseq . i).| to_power p by Def1;
hence (rseq rto_power p) . i >= 0 by ; :: thesis: verum
end;
then ((Sum (rseq rto_power p)) to_power (1 / p)) to_power p = (Sum (rseq rto_power p)) to_power ((1 / p) * p) by
.= (Sum (rseq rto_power p)) to_power 1 by
.= Sum (rseq rto_power p) by POWER:25 ;
then A6: Sum (rseq rto_power p) = 0 by ;
now :: thesis: for n being Nat holds rseq . n = 0
let n be Nat; :: thesis: rseq . n = 0
reconsider n9 = n as Nat ;
A7: 0 to_power (1 / p) = 0 by ;
(rseq rto_power p) . n9 = |.(rseq . n9).| to_power p by Def1;
then A8: |.(rseq . n).| to_power p = 0 by ;
(|.(rseq . n).| to_power p) to_power (1 / p) = |.(rseq . n).| to_power (p * (1 / p)) by
.= |.(rseq . n).| to_power 1 by
.= |.(rseq . n).| by POWER:25 ;
hence rseq . n = 0 by ; :: thesis: verum
end;
hence for n being Nat holds rseq . n = 0 ; :: thesis: verum