theorem Th12: :: EUCLIDLP:12

for a being Real
for n being Nat
for x, y being Element of REAL n holds
( a * (x - y) = (a * x) + (- (a * y)) & a * (x - y) = (a * x) + ((- a) * y) & a * (x - y) = (a * x) - (a * y) )