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
|.p.| = 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
|.p.| = sqrt ((((f1 . t) ^2 ) + ((f2 . t) ^2 )) + ((f3 . t) ^2 ))
let t be Real; :: thesis: ( p = (VFunc f1,f2,f3) . t implies |.p.| = sqrt ((((f1 . t) ^2 ) + ((f2 . t) ^2 )) + ((f3 . t) ^2 )) )
assume A1: p = (VFunc f1,f2,f3) . t ; :: thesis: |.p.| = sqrt ((((f1 . t) ^2 ) + ((f2 . t) ^2 )) + ((f3 . t) ^2 ))
reconsider f = p as FinSequence of REAL ;
|.p.| = sqrt (Sum <*((f1 . t) * (f1 . t)),((f2 . t) * (f2 . t)),((f3 . t) * (f3 . t))*>) by A1, Th36
.= sqrt ((((f1 . t) ^2 ) + ((f2 . t) ^2 )) + ((f3 . t) ^2 )) by RVSUM_1:108 ;
hence |.p.| = sqrt ((((f1 . t) ^2 ) + ((f2 . t) ^2 )) + ((f3 . t) ^2 )) ; :: thesis: verum