let seq1, seq2 be Complex_Sequence; :: thesis: ( ( for n being Element of NAT holds
( 0 <= |.seq1.| . n & |.seq1.| . n <= |.seq2.| . n ) ) & seq2 is absolutely_summable implies ( seq1 is absolutely_summable & Sum |.seq1.| <= Sum |.seq2.| ) )
assume A1: ( ( for n being Element of NAT holds
( 0 <= |.seq1.| . n & |.seq1.| . n <= |.seq2.| . n ) ) & seq2 is absolutely_summable ) ; :: thesis: ( seq1 is absolutely_summable & Sum |.seq1.| <= Sum |.seq2.| )
thus ( |.seq1.| is summable & Sum |.seq1.| <= Sum |.seq2.| ) by A1, SERIES_1:24; :: according to COMSEQ_3:def 11 :: thesis: verum