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 natural number 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 natural number holds rseq . n = 0
A2: 1 / p > 0 by A1, XREAL_1:141;
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 natural number 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 natural number holds rseq . n = 0
A5: for i being Element of NAT holds (rseq rto_power p) . i >= 0

proof

let i be Element of NAT ; :: thesis: (rseq rto_power p) . i >= 0
(rseq rto_power p) . i = (abs (rseq . i)) to_power p by Def1;
hence (rseq rto_power p) . i >= 0 by A1, Lm1, COMPLEX1:132; :: 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 A1, A2, A3, HOLDER_1:2, SERIES_1:21
.= (Sum (rseq rto_power p)) to_power 1 by A1, XCMPLX_1:107
.= Sum (rseq rto_power p) by POWER:30 ;
then A6: Sum (rseq rto_power p) = 0 by A1, A4, POWER:def 2;

now

let n be natural number ; :: thesis: rseq . n = 0
reconsider n9 = n as Element of NAT by ORDINAL1:def 13;
A7: 0 to_power (1 / p) = 0 by A2, POWER:def 2;
(rseq rto_power p) . n9 = (abs (rseq . n9)) to_power p by Def1;
then A8: (abs (rseq . n)) to_power p = 0 by A3, A5, A6, RSSPACE:21;
((abs (rseq . n)) to_power p) to_power (1 / p) = (abs (rseq . n)) to_power (p * (1 / p)) by A1, A2, COMPLEX1:132, HOLDER_1:2
.= (abs (rseq . n)) to_power 1 by A1, XCMPLX_1:107
.= abs (rseq . n) by POWER:30 ;
hence rseq . n = 0 by A8, A7, ABSVALUE:7; :: thesis: verum

end;

hence for n being natural number holds rseq . n = 0 ; :: thesis: verum