take NAT --> 0c ; :: thesis: NAT --> 0c is absolutely_summable
for n being Nat holds (NAT --> 0c) . n = 0c ;
hence NAT --> 0c is absolutely_summable by Th51; :: thesis: verum