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

take C ; :: thesis: C is norm_summable

for n being Nat holds C . n = 0. X by ORDINAL1:def 12, FUNCOP_1:7;

hence C is norm_summable by Th13; :: thesis: verum

take C ; :: thesis: C is norm_summable

for n being Nat holds C . n = 0. X by ORDINAL1:def 12, FUNCOP_1:7;

hence C is norm_summable by Th13; :: thesis: verum