reconsider C = NAT --> (0. X) as sequence of X ;
take C ; :: thesis: C is summable
take 0. X ; :: according to CLVECT_1:def 15,CLOPBAN3:def 1 :: thesis: for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= ||.(((Partial_Sums C) . b₃) - (0. X)).|| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= ||.(((Partial_Sums C) . b₂) - (0. X)).|| ) )
assume A1: 0 < p ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= ||.(((Partial_Sums C) . b₂) - (0. X)).|| )
take 0 ; :: thesis: for b₁ being set holds
( not 0 <= b₁ or not p <= ||.(((Partial_Sums C) . b₁) - (0. X)).|| )
let m be 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 Nat holds C . n = 0. X by ORDINAL1:def 12, FUNCOP_1:7;
then ||.(((Partial_Sums C) . m) - (0. X)).|| = ||.((0. X) - (0. X)).|| by Th1
.= 0 by CLVECT_1:107 ;
hence not p <= ||.(((Partial_Sums C) . m) - (0. X)).|| by A1; :: thesis: verum