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 ))]|
A1: (x * p) `1 = x * (p `1 ) by RVSUM_1:66;
A2: (x * p) `2 = x * (p `2 ) by RVSUM_1:66;
(x * p) `3 = x * (p `3 ) by RVSUM_1:66;
hence x * p = |[(x * (p `1 )),(x * (p `2 )),(x * (p `3 ))]| by A1, A2, Th3; :: thesis: verum