reconsider C = NAT --> (0. X) as sequence of X ;
take C ; :: thesis: C is summable
take 0. X ; :: according to NORMSP_1:def 9,LOPBAN_3:def 2 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= ||.(((Partial_Sums C) . b₃) - (0. X)).|| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= ||.(((Partial_Sums C) . b₂) - (0. X)).|| ) )
assume A1: 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= ||.(((Partial_Sums C) . b₂) - (0. X)).|| )
take 0 ; :: thesis: for b₁ being Element of NAT holds
( not 0 <= b₁ or not p <= ||.(((Partial_Sums C) . b₁) - (0. X)).|| )
let m be Element of NAT ; :: thesis: ( not 0 <= m or not p <= ||.(((Partial_Sums C) . m) - (0. X)).|| )
assume 0 <= m ; :: thesis: not p <= ||.(((Partial_Sums C) . m) - (0. X)).||
for n being Element of NAT holds C . n = 0. X by FUNCOP_1:13;
then ||.(((Partial_Sums C) . m) - (0. X)).|| = ||.((0. X) - (0. X)).|| by Th1
.= 0 by NORMSP_1:10 ;
hence not p <= ||.(((Partial_Sums C) . m) - (0. X)).|| by A1; :: thesis: verum