let x be real number ; :: thesis: for p being Point of (TOP-REAL 2) holds x * p = |[(x * (p `1 )),(x * (p `2 ))]|
let p be Point of (TOP-REAL 2); :: thesis: x * p = |[(x * (p `1 )),(x * (p `2 ))]|
( (x * p) `1 = x * (p `1 ) & (x * p) `2 = x * (p `2 ) ) by RVSUM_1:66;
hence x * p = |[(x * (p `1 )),(x * (p `2 ))]| by Th57; :: thesis: verum