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).| = (abs r) * (sqrt ((((f1 . t) ^2 ) + ((f2 . t) ^2 )) + ((f3 . t) ^2 )))
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).| = (abs r) * (sqrt ((((f1 . t) ^2 ) + ((f2 . t) ^2 )) + ((f3 . t) ^2 )))
let f1, f2, f3 be PartFunc of ,; :: thesis: for t being Real st p = (VFunc f1,f2,f3) . t holds
|.(r * p).| = (abs r) * (sqrt ((((f1 . t) ^2 ) + ((f2 . t) ^2 )) + ((f3 . t) ^2 )))
let t be Real; :: thesis: ( p = (VFunc f1,f2,f3) . t implies |.(r * p).| = (abs r) * (sqrt ((((f1 . t) ^2 ) + ((f2 . t) ^2 )) + ((f3 . t) ^2 ))) )
assume A1: p = (VFunc f1,f2,f3) . t ; :: thesis: |.(r * p).| = (abs r) * (sqrt ((((f1 . t) ^2 ) + ((f2 . t) ^2 )) + ((f3 . t) ^2 )))
reconsider f = p as FinSequence of REAL ;
|.(r * p).| = (abs r) * |.p.| by EUCLID:14
.= (abs r) * (sqrt ((((f1 . t) ^2 ) + ((f2 . t) ^2 )) + ((f3 . t) ^2 ))) by A1, Th53 ;
hence |.(r * p).| = (abs r) * (sqrt ((((f1 . t) ^2 ) + ((f2 . t) ^2 )) + ((f3 . t) ^2 ))) ; :: thesis: verum