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 )))
reconsider f = p as FinSequence of REAL ;
|.(r * p).| = (abs r) * |.p.| by EUCLID:14
.= (abs r) * (sqrt ((((p . 1) ^2 ) + ((p . 2) ^2 )) + ((p . 3) ^2 ))) by Th53 ;
hence |.(r * p).| = (abs r) * (sqrt ((((p . 1) ^2 ) + ((p . 2) ^2 )) + ((p . 3) ^2 ))) ; :: thesis: verum