let r be Real; :: thesis: for p being Element of REAL 3 holds |.(r * p).| = |.r.| * (sqrt ((((p . 1) ^2) + ((p . 2) ^2)) + ((p . 3) ^2)))
let p be Element of REAL 3; :: thesis: |.(r * p).| = |.r.| * (sqrt ((((p . 1) ^2) + ((p . 2) ^2)) + ((p . 3) ^2)))
|.(r * p).| = |.r.| * |.p.| by EUCLID:11
.= |.r.| * (sqrt ((((p . 1) ^2) + ((p . 2) ^2)) + ((p . 3) ^2))) by Th56 ;
hence |.(r * p).| = |.r.| * (sqrt ((((p . 1) ^2) + ((p . 2) ^2)) + ((p . 3) ^2))) ; :: thesis: verum