let r be Real; :: thesis: for p being Point of holds r * p = |[(r * (p `1 )),(r * (p `2 ))]|
let p be Point of ; :: 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