let r1, r2 be Element of REAL ; :: thesis: for p being Element of REAL 3 holds (r1 * p) + (r2 * p) = (r1 + r2) * |[(p . 1),(p . 2),(p . 3)]|
let p be Element of REAL 3; :: thesis: (r1 * p) + (r2 * p) = (r1 + r2) * |[(p . 1),(p . 2),(p . 3)]|
(r1 * p) + (r2 * p) = (r1 + r2) * p by RVSUM_1:72;
hence (r1 * p) + (r2 * p) = (r1 + r2) * |[(p . 1),(p . 2),(p . 3)]| by Lm1; :: thesis: verum