for r, p being Real
for n being Element of NAT holds (r * p) (#) ((#Z n) ^) = r (#) (p (#) ((#Z n) ^))