for x being Real
for m, n being Nat holds x #Z (n + m) = (x #Z n) * (x #Z m)