let r be Real; :: thesis: for p, q being Element of REAL 3 holds |((r * p),q)| = r * ((((p . 1) * (q . 1)) + ((p . 2) * (q . 2))) + ((p . 3) * (q . 3)))
let p, q be Element of REAL 3; :: thesis: |((r * p),q)| = r * ((((p . 1) * (q . 1)) + ((p . 2) * (q . 2))) + ((p . 3) * (q . 3)))
|((r * p),q)| = r * |(p,q)| by RVSUM_1:131;
hence |((r * p),q)| = r * ((((p . 1) * (q . 1)) + ((p . 2) * (q . 2))) + ((p . 3) * (q . 3))) by Lm5; :: thesis: verum