let x be Real; :: thesis: for p being Point of (TOP-REAL 3) holds x * p = |[(x * (p `1)),(x * (p `2)),(x * (p `3))]|
let p be Point of (TOP-REAL 3); :: thesis: x * p = |[(x * (p `1)),(x * (p `2)),(x * (p `3))]|
reconsider q = p as Element of REAL 3 by EUCLID:22;
(x * q) . 2 = x * (q . 2) by RVSUM_1:44;
then A1: (x * p) `2 = x * (p `2) ;
(x * q) . 3 = x * (q . 3) by RVSUM_1:44;
then A2: (x * p) `3 = x * (p `3) ;
(x * q) . 1 = x * (q . 1) by RVSUM_1:44;
then (x * p) `1 = x * (p `1) ;
hence x * p = |[(x * (p `1)),(x * (p `2)),(x * (p `3))]| by A1, A2, Th3; :: thesis: verum