theorem Th11: :: EUCLIDLP:11

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