let r 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
r * p = |[(r * (f1 . t)),(r * (f2 . t)),(r * (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
r * p = |[(r * (f1 . t)),(r * (f2 . t)),(r * (f3 . t))]|
let f1, f2, f3 be PartFunc of ,; :: thesis: for t being Real st p = (VFunc f1,f2,f3) . t holds
r * p = |[(r * (f1 . t)),(r * (f2 . t)),(r * (f3 . t))]|
let t be Real; :: thesis: ( p = (VFunc f1,f2,f3) . t implies r * p = |[(r * (f1 . t)),(r * (f2 . t)),(r * (f3 . t))]| )
assume A1: p = (VFunc f1,f2,f3) . t ; :: thesis: r * p = |[(r * (f1 . t)),(r * (f2 . t)),(r * (f3 . t))]|
r * p = |[(r * (p . 1)),(r * (p . 2)),(r * (p . 3))]| by Lm3
.= |[(r * (f1 . t)),(r * (p . 2)),(r * (p . 3))]| by A1, Th34
.= |[(r * (f1 . t)),(r * (f2 . t)),(r * (p . 3))]| by A1, Th34
.= |[(r * (f1 . t)),(r * (f2 . t)),(r * (f3 . t))]| by A1, Th34 ;
hence r * p = |[(r * (f1 . t)),(r * (f2 . t)),(r * (f3 . t))]| ; :: thesis: verum