let r1, r2 be Element of REAL ; :: thesis: for p being Element of REAL 3
for f1, f2, f3 being PartFunc of ,
for t being Real st p = (VFunc f1,f2,f3) . t holds
(r1 * p) - (r2 * p) = (r1 - r2) * |[(f1 . t),(f2 . t),(f3 . t)]|
let p be Element of REAL 3; :: thesis: for f1, f2, f3 being PartFunc of ,
for t being Real st p = (VFunc f1,f2,f3) . t holds
(r1 * p) - (r2 * p) = (r1 - r2) * |[(f1 . t),(f2 . t),(f3 . t)]|
let f1, f2, f3 be PartFunc of ,; :: thesis: for t being Real st p = (VFunc f1,f2,f3) . t holds
(r1 * p) - (r2 * p) = (r1 - r2) * |[(f1 . t),(f2 . t),(f3 . t)]|
let t be Real; :: thesis: ( p = (VFunc f1,f2,f3) . t implies (r1 * p) - (r2 * p) = (r1 - r2) * |[(f1 . t),(f2 . t),(f3 . t)]| )
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:71
.= (r1 + (- r2)) * R by RVSUM_1:72 ;
hence (r1 * R) - (r2 * R) = (r1 - r2) * R ; :: thesis: verum

end;

then (r1 * p) - (r2 * p) = (r1 - r2) * p ;
hence ( p = (VFunc f1,f2,f3) . t implies (r1 * p) - (r2 * p) = (r1 - r2) * |[(f1 . t),(f2 . t),(f3 . t)]| ) by Def1; :: thesis: verum