theorem Th21: :: EUCLIDLP:21

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