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