theorem :: EUCLID_8:69

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)]|