reconsider C = NAT --> (0. X) as sequence of X ;
A1: for n being Element of NAT holds C . n = 0. X by FUNCOP_1:13;
take C ; :: thesis: C is norm_summable
thus C is norm_summable by A1, Th18; :: thesis: verum