let X be RealNormSpace; :: thesis: for seq being sequence of X
for rseq1 being Real_Sequence st ||.seq.|| is non-increasing & ( for n being Nat holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) holds
( seq is norm_summable iff rseq1 is summable )
let seq be sequence of X; :: thesis: for rseq1 being Real_Sequence st ||.seq.|| is non-increasing & ( for n being Nat holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) holds
( seq is norm_summable iff rseq1 is summable )
let rseq1 be Real_Sequence; :: thesis: ( ||.seq.|| is non-increasing & ( for n being Nat holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) implies ( seq is norm_summable iff rseq1 is summable ) )
assume ( ||.seq.|| is non-increasing & ( for n being Nat holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) ) ; :: thesis: ( seq is norm_summable iff rseq1 is summable )
then for n being Nat holds
( ||.seq.|| is non-increasing & ||.seq.|| . n >= 0 & rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) by Th2;
then ( ||.seq.|| is summable iff rseq1 is summable ) by SERIES_1:31;
hence ( seq is norm_summable iff rseq1 is summable ) ; :: thesis: verum