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