theorem :: ARYTM_0:15

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