theorem Th13: :: EUCLIDLP:13

for s, t, u being Real
for n being Nat
for x being Element of REAL n holds ((s - t) - u) * x = ((s * x) - (t * x)) - (u * x)