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