reconsider C = NAT --> (0. X) as sequence of X ;
take C ; :: thesis: C is norm_summable
for n being Element of NAT holds C . n = 0. X by FUNCOP_1:7;
hence C is norm_summable by Th17; :: thesis: verum