let X be RealBanachSpace; :: thesis: for s being sequence of X st s is norm_summable holds
||.(Sum s).|| <= Sum ||.s.||
let s be sequence of X; :: thesis: ( s is norm_summable implies ||.(Sum s).|| <= Sum ||.s.|| )
assume A1: s is norm_summable ; :: thesis: ||.(Sum s).|| <= Sum ||.s.||
then A3: ||.s.|| is summable ;
A5: now :: thesis: for k being Nat holds ||.(Partial_Sums s).|| . k <= (Partial_Sums ||.s.||) . k
let k be Nat; :: thesis: ||.(Partial_Sums s).|| . k <= (Partial_Sums ||.s.||) . k
||.(Partial_Sums s).|| . k = ||.((Partial_Sums s) . k).|| by NORMSP_0:def 4;
hence ||.(Partial_Sums s).|| . k <= (Partial_Sums ||.s.||) . k by LOPBAN410; :: thesis: verum
end;
A6: s is summable by A1;
then A8: ||.(Partial_Sums s).|| is convergent by NORMSP_1:23;
lim ||.(Partial_Sums s).|| = ||.(Sum s).|| by A6, LOPBAN_1:20;
hence ||.(Sum s).|| <= Sum ||.s.|| by A3, A5, A8, SEQ_2:18; :: thesis: verum