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,p)| = (((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,p)| = (((f1 . t) ^2 ) + ((f2 . t) ^2 )) + ((f3 . t) ^2 )
let t be Real; :: thesis: ( p = (VFunc f1,f2,f3) . t implies |(p,p)| = (((f1 . t) ^2 ) + ((f2 . t) ^2 )) + ((f3 . t) ^2 ) )
assume p = (VFunc f1,f2,f3) . t ; :: thesis: |(p,p)| = (((f1 . t) ^2 ) + ((f2 . t) ^2 )) + ((f3 . t) ^2 )
then p = |[(f1 . t),(f2 . t),(f3 . t)]| by Def1;
hence |(p,p)| = (((f1 . t) ^2 ) + ((f2 . t) ^2 )) + ((f3 . t) ^2 ) by LmTh8; :: thesis: verum