let X be RealNormSpace; :: thesis: for seq being sequence of X holds
( Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable )
let seq be sequence of X; :: thesis: ( Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable )
for n being Nat holds 0 <= ||.seq.|| . n by Th2;
then ( Partial_Sums ||.seq.|| is bounded_above iff ||.seq.|| is summable ) by SERIES_1:17;
hence ( Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable ) ; :: thesis: verum