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

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