let X be RealNormSpace; :: thesis: for seq being sequence of X st ( for n being Nat holds seq . n = 0. X ) holds

seq is norm_summable

let seq be sequence of X; :: thesis: ( ( for n being Nat holds seq . n = 0. X ) implies seq is norm_summable )

assume A1: for n being Nat holds seq . n = 0. X ; :: thesis: seq is norm_summable

take 0 ; :: according to SEQ_2:def 6,SERIES_1:def 2,LOPBAN_3:def 3 :: thesis: for b_{1} being object holds

( b_{1} <= 0 or ex b_{2} being set st

for b_{3} being set holds

( not b_{2} <= b_{3} or not b_{1} <= |.(((Partial_Sums ||.seq.||) . b_{3}) - 0).| ) )

let p be Real; :: thesis: ( p <= 0 or ex b_{1} being set st

for b_{2} being set holds

( not b_{1} <= b_{2} or not p <= |.(((Partial_Sums ||.seq.||) . b_{2}) - 0).| ) )

assume A2: 0 < p ; :: thesis: ex b_{1} being set st

for b_{2} being set holds

( not b_{1} <= b_{2} or not p <= |.(((Partial_Sums ||.seq.||) . b_{2}) - 0).| )

take 0 ; :: thesis: for b_{1} being set holds

( not 0 <= b_{1} or not p <= |.(((Partial_Sums ||.seq.||) . b_{1}) - 0).| )

let m be Nat; :: thesis: ( not 0 <= m or not p <= |.(((Partial_Sums ||.seq.||) . m) - 0).| )

assume 0 <= m ; :: thesis: not p <= |.(((Partial_Sums ||.seq.||) . m) - 0).|

|.(((Partial_Sums ||.seq.||) . m) - 0).| = |.(0 - 0).| by A1, Th6

.= 0 by ABSVALUE:def 1 ;

hence not p <= |.(((Partial_Sums ||.seq.||) . m) - 0).| by A2; :: thesis: verum

seq is norm_summable

let seq be sequence of X; :: thesis: ( ( for n being Nat holds seq . n = 0. X ) implies seq is norm_summable )

assume A1: for n being Nat holds seq . n = 0. X ; :: thesis: seq is norm_summable

take 0 ; :: according to SEQ_2:def 6,SERIES_1:def 2,LOPBAN_3:def 3 :: thesis: for b

( b

for b

( not b

let p be Real; :: thesis: ( p <= 0 or ex b

for b

( not b

assume A2: 0 < p ; :: thesis: ex b

for b

( not b

take 0 ; :: thesis: for b

( not 0 <= b

let m be Nat; :: thesis: ( not 0 <= m or not p <= |.(((Partial_Sums ||.seq.||) . m) - 0).| )

assume 0 <= m ; :: thesis: not p <= |.(((Partial_Sums ||.seq.||) . m) - 0).|

|.(((Partial_Sums ||.seq.||) . m) - 0).| = |.(0 - 0).| by A1, Th6

.= 0 by ABSVALUE:def 1 ;

hence not p <= |.(((Partial_Sums ||.seq.||) . m) - 0).| by A2; :: thesis: verum