let X be ComplexNormSpace; :: thesis: for rseq1 being Real_Sequence
for seq2 being sequence of X st rseq1 is summable & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(seq2 . n).|| <= rseq1 . n holds
seq2 is norm_summable
let rseq1 be Real_Sequence; :: thesis: for seq2 being sequence of X st rseq1 is summable & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(seq2 . n).|| <= rseq1 . n holds
seq2 is norm_summable
let seq2 be sequence of X; :: thesis: ( rseq1 is summable & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(seq2 . n).|| <= rseq1 . n implies seq2 is norm_summable )
assume that
A1: rseq1 is summable and
A2: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(seq2 . n).|| <= rseq1 . n ; :: thesis: seq2 is norm_summable
consider m being Element of NAT such that
A3: for n being Element of NAT st m <= n holds
||.(seq2 . n).|| <= rseq1 . n by A2;

A4: now

let n be Element of NAT ; :: thesis: 0 <= ||.seq2.|| . n
||.(seq2 . n).|| = ||.seq2.|| . n by NORMSP_0:def 4;
hence 0 <= ||.seq2.|| . n by CLVECT_1:105; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: ( m <= n implies ||.seq2.|| . n <= rseq1 . n )
assume m <= n ; :: thesis: ||.seq2.|| . n <= rseq1 . n
then ||.(seq2 . n).|| <= rseq1 . n by A3;
hence ||.seq2.|| . n <= rseq1 . n by NORMSP_0:def 4; :: thesis: verum

end;

hence ||.seq2.|| is summable by A1, A4, SERIES_1:19; :: according to CLOPBAN3:def 3 :: thesis: verum