f (#) (NAT --> a) = f * a by Th8;
hence f * a is convergent by NDIFF_1:13, NDIFF_1:18; :: thesis: verum