let r be Real; :: thesis: for p being Point of (TOP-REAL 2) holds r * p = |[(r * (p `1)),(r * (p `2))]|
let p be Point of (TOP-REAL 2); :: thesis: r * p = |[(r * (p `1)),(r * (p `2))]|
p = |[(p `1),(p `2)]| by EUCLID:53;
hence r * p = |[(r * (p `1)),(r * (p `2))]| by EUCLID:58; :: thesis: verum