theorem :: LOPBAN_3:28

for X being RealNormSpace
for seq1, seq2 being sequence of X st ( for n being Nat holds
( 0 <= ||.seq1.|| . n & ||.seq1.|| . n <= ||.seq2.|| . n ) ) & seq2 is norm_summable holds
( seq1 is norm_summable & Sum ||.seq1.|| <= Sum ||.seq2.|| ) by SERIES_1:20;