let a be Real; :: thesis: for u, v being Element of (TOP-REAL 3) holds
( a * |(u,v)| = |((a * u),v)| & a * |(u,v)| = |(u,(a * v))| )
let u, v be Element of (TOP-REAL 3); :: thesis: ( a * |(u,v)| = |((a * u),v)| & a * |(u,v)| = |(u,(a * v))| )
A1: a * (u `1) = a * (u . 1) by EUCLID_5:def 1
.= (a * u) . 1 by RVSUM_1:44
.= (a * u) `1 by EUCLID_5:def 1 ;
A2: a * (u `2) = a * (u . 2) by EUCLID_5:def 2
.= (a * u) . 2 by RVSUM_1:44
.= (a * u) `2 by EUCLID_5:def 2 ;
A3: a * (u `3) = a * (u . 3) by EUCLID_5:def 3
.= (a * u) . 3 by RVSUM_1:44
.= (a * u) `3 by EUCLID_5:def 3 ;
thus a * |(u,v)| = a * ((((u `1) * (v `1)) + ((u `2) * (v `2))) + ((u `3) * (v `3))) by EUCLID_5:29
.= ((((a * u) `1) * (v `1)) + (((a * u) `2) * (v `2))) + (((a * u) `3) * (v `3)) by A1, A2, A3
.= |((a * u),v)| by EUCLID_5:29 ; :: thesis: a * |(u,v)| = |(u,(a * v))|
A4: a * (v `1) = a * (v . 1) by EUCLID_5:def 1
.= (a * v) . 1 by RVSUM_1:44
.= (a * v) `1 by EUCLID_5:def 1 ;
A5: a * (v `2) = a * (v . 2) by EUCLID_5:def 2
.= (a * v) . 2 by RVSUM_1:44
.= (a * v) `2 by EUCLID_5:def 2 ;
A6: a * (v `3) = a * (v . 3) by EUCLID_5:def 3
.= (a * v) . 3 by RVSUM_1:44
.= (a * v) `3 by EUCLID_5:def 3 ;
thus a * |(u,v)| = a * ((((u `1) * (v `1)) + ((u `2) * (v `2))) + ((u `3) * (v `3))) by EUCLID_5:29
.= (((u `1) * ((a * v) `1)) + ((u `2) * ((a * v) `2))) + ((u `3) * ((a * v) `3)) by A4, A5, A6
.= |(u,(a * v))| by EUCLID_5:29 ; :: thesis: verum