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