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)]| )
(r1 * p) + (r2 * p) = (r1 + r2) * p by RVSUM_1:72;
hence ( p = (VFunc f1,f2,f3) . t implies (r1 * p) + (r2 * p) = (r1 + r2) * |[(f1 . t),(f2 . t),(f3 . t)]| ) by Def1; :: thesis: verum