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