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 b1 being object holds
( b1 <= 0 or ex b2 being set st
for b3 being set holds
( not b2 <= b3 or not b1 <= |.((() . b3) - 0).| ) )

let p be Real; :: thesis: ( p <= 0 or ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not p <= |.((() . b2) - 0).| ) )

assume A2: 0 < p ; :: thesis: ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not p <= |.((() . b2) - 0).| )

take 0 ; :: thesis: for b1 being set holds
( not 0 <= b1 or not p <= |.((() . b1) - 0).| )

let m be Nat; :: thesis: ( not 0 <= m or not p <= |.((() . m) - 0).| )
assume 0 <= m ; :: thesis: not p <= |.((() . m) - 0).|
|.((() . m) - 0).| = |.().| by
.= 0 by ABSVALUE:def 1 ;
hence not p <= |.((() . m) - 0).| by A2; :: thesis: verum