for a being Real
for k, l being Integer st a <> 0 holds
a #Z (k + l) = (a #Z k) * (a #Z l)