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)]|
for R being Element of 3 -tuples_on REAL holds (r1 * R) - (r2 * R) = (r1 - r2) * R

proof

let R be Element of 3 -tuples_on REAL; :: thesis: (r1 * R) - (r2 * R) = (r1 - r2) * R
(r1 * R) - (r2 * R) = (r1 * R) + (((- 1) * r2) * R) by RVSUM_1:49
.= (r1 + (- r2)) * R by RVSUM_1:50 ;
hence (r1 * R) - (r2 * R) = (r1 - r2) * R ; :: thesis: verum

end;

then (r1 * p) - (r2 * p) = (r1 - r2) * p ;
hence (r1 * p) - (r2 * p) = (r1 - r2) * |[(p . 1),(p . 2),(p . 3)]| by Th1; :: thesis: verum