theorem Th20: :: EUCLIDLP:20

for a being Real
for n being Nat
for x1, x2, x3 being Element of REAL n holds a * ((x1 + x2) + x3) = ((a * x1) + (a * x2)) + (a * x3)