theorem Th3: :: EUCLIDLP:3

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