theorem Th22: :: EUCLIDLP:22

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