take NAT --> 0c ; :: thesis: NAT --> 0c is absolutely_summable
for n being Element of NAT holds (NAT --> 0c ) . n = 0c by FUNCOP_1:13;
hence NAT --> 0c is absolutely_summable by Th52; :: thesis: verum