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:57;
hence r * p = |[(r * (p `1 )),(r * (p `2 ))]| by EUCLID:62; :: thesis: verum