let X be ComplexNormSpace; :: thesis: for seq1, seq2 being sequence of X st ( for n being Element of NAT holds
( 0 <= ||.seq1.|| . n & ||.seq1.|| . n <= ||.seq2.|| . n ) ) & seq2 is norm_summable holds
( seq1 is norm_summable & Sum ||.seq1.|| <= Sum ||.seq2.|| )
let seq1, seq2 be sequence of X; :: thesis: ( ( for n being Element of NAT holds
( 0 <= ||.seq1.|| . n & ||.seq1.|| . n <= ||.seq2.|| . n ) ) & seq2 is norm_summable implies ( seq1 is norm_summable & Sum ||.seq1.|| <= Sum ||.seq2.|| ) )
assume ( ( for n being Element of NAT holds
( 0 <= ||.seq1.|| . n & ||.seq1.|| . n <= ||.seq2.|| . n ) ) & seq2 is norm_summable ) ; :: thesis: ( seq1 is norm_summable & Sum ||.seq1.|| <= Sum ||.seq2.|| )
hence ( ||.seq1.|| is summable & Sum ||.seq1.|| <= Sum ||.seq2.|| ) by SERIES_1:20; :: according to CLOPBAN3:def 3 :: thesis: verum