theorem :: RVSUM_4:26

for c being Complex holds 0 (#) (NAT --> c) = NAT --> 0