let X be RealNormSpace; :: thesis: for rseq1 being Real_Sequence

for seq2 being sequence of X st rseq1 is summable & ex m being Nat st

for n being 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 Nat st

for n being 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 Nat st

for n being 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 Nat st

for n being Nat st m <= n holds

||.(seq2 . n).|| <= rseq1 . n ; :: thesis: seq2 is norm_summable

consider m being Nat such that

A3: for n being Nat st m <= n holds

||.(seq2 . n).|| <= rseq1 . n by A2;

for seq2 being sequence of X st rseq1 is summable & ex m being Nat st

for n being 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 Nat st

for n being 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 Nat st

for n being 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 Nat st

for n being Nat st m <= n holds

||.(seq2 . n).|| <= rseq1 . n ; :: thesis: seq2 is norm_summable

consider m being Nat such that

A3: for n being Nat st m <= n holds

||.(seq2 . n).|| <= rseq1 . n by A2;

A4: now :: thesis: for n being Nat holds 0 <= ||.seq2.|| . n

let n be Nat; :: thesis: 0 <= ||.seq2.|| . n

||.(seq2 . n).|| = ||.seq2.|| . n by NORMSP_0:def 4;

hence 0 <= ||.seq2.|| . n ; :: thesis: verum

end;||.(seq2 . n).|| = ||.seq2.|| . n by NORMSP_0:def 4;

hence 0 <= ||.seq2.|| . n ; :: thesis: verum

now :: thesis: for n being Nat st m <= n holds

||.seq2.|| . n <= rseq1 . n

hence
||.seq2.|| is summable
by A1, A4, SERIES_1:19; :: according to LOPBAN_3:def 3 :: thesis: verum||.seq2.|| . n <= rseq1 . n

let n be 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;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