let r be Element of REAL ; :: thesis: for p1, p2 being Element of REAL 3 holds |((r * p1),p2)| = r * |(p1,p2)|
let p1, p2 be Element of REAL 3; :: thesis: |((r * p1),p2)| = r * |(p1,p2)|
A1: r * p1 = |[(r * (p1 . 1)),(r * (p1 . 2)),(r * (p1 . 3))]| by Lm1;
A2: r * |(p1,p2)| = r * ((((p1 . 1) * (p2 . 1)) + ((p1 . 2) * (p2 . 2))) + ((p1 . 3) * (p2 . 3))) by Lm9;
A3: ((r * p1) . 1) * (p2 . 1) = (r * (p1 . 1)) * (p2 . 1) by A1, FINSEQ_1:45
.= r * ((p1 . 1) * (p2 . 1)) ;
A4: ((r * p1) . 2) * (p2 . 2) = (r * (p1 . 2)) * (p2 . 2) by A1, FINSEQ_1:45
.= r * ((p1 . 2) * (p2 . 2)) ;
((r * p1) . 3) * (p2 . 3) = (r * (p1 . 3)) * (p2 . 3) by A1, FINSEQ_1:45
.= r * ((p1 . 3) * (p2 . 3)) ;
then |((r * p1),p2)| = ((r * ((p1 . 1) * (p2 . 1))) + (r * ((p1 . 2) * (p2 . 2)))) + (r * ((p1 . 3) * (p2 . 3))) by A3, A4, Lm9;
hence |((r * p1),p2)| = r * |(p1,p2)| by A2; :: thesis: verum