theorem :: EUCLID_8:67

for r1, r2 being Real
for p being Element of REAL 3 holds (r1 * p) + (r2 * p) = (r1 + r2) * |[(p . 1),(p . 2),(p . 3)]|