let X be RealNormSpace; :: thesis: for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds
seq is norm_summable
let seq be sequence of X; :: thesis: ( ( for n being Element of NAT holds seq . n = 0. X ) implies seq is norm_summable )
assume A1: for n being Element of 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₁ being set holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= abs (((Partial_Sums ||.seq.||) . b₃) - 0) ) )
let p be real number ; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs (((Partial_Sums ||.seq.||) . b₂) - 0) ) )
assume A2: 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs (((Partial_Sums ||.seq.||) . b₂) - 0) )
take 0 ; :: thesis: for b₁ being Element of NAT holds
( not 0 <= b₁ or not p <= abs (((Partial_Sums ||.seq.||) . b₁) - 0) )
let m be Element of NAT ; :: thesis: ( not 0 <= m or not p <= abs (((Partial_Sums ||.seq.||) . m) - 0) )
assume 0 <= m ; :: thesis: not p <= abs (((Partial_Sums ||.seq.||) . m) - 0)
abs (((Partial_Sums ||.seq.||) . m) - 0) = abs (0 - 0) by A1, Th6
.= 0 by ABSVALUE:def 1 ;
hence not p <= abs (((Partial_Sums ||.seq.||) . m) - 0) by A2; :: thesis: verum