let r1, r2 be 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:50;
hence (r1 * p) + (r2 * p) = (r1 + r2) * |[(p . 1),(p . 2),(p . 3)]| by Th1; :: thesis: verum