reconsider C = NAT --> (0. X) as sequence of X ;

take C ; :: thesis: C is summable

take 0. X ; :: according to NORMSP_1:def 6,LOPBAN_3:def 1 :: 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 C) . b_{3}) - (0. X)).|| ) )

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 C) . b_{2}) - (0. X)).|| ) )

assume A1: 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 C) . b_{2}) - (0. X)).|| )

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

( not 0 <= b_{1} or not p <= ||.(((Partial_Sums C) . b_{1}) - (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 NORMSP_1:6 ;

hence not p <= ||.(((Partial_Sums C) . m) - (0. X)).|| by A1; :: thesis: verum

take C ; :: thesis: C is summable

take 0. X ; :: according to NORMSP_1:def 6,LOPBAN_3:def 1 :: thesis: for b

( b

for b

( not b

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

for b

( not b

assume A1: 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 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 NORMSP_1:6 ;

hence not p <= ||.(((Partial_Sums C) . m) - (0. X)).|| by A1; :: thesis: verum