theorem :: ARYTM_2:13

for x, y, z being Element of REAL+ holds x *' (y + z) = (x *' y) + (x *' z)