let p, q be Point of (TOP-REAL 2); :: thesis: for r being Real holds dist ((r * p),(r * q)) = |.r.| * (dist (p,q))
let r be Real; :: thesis: dist ((r * p),(r * q)) = |.r.| * (dist (p,q))
thus dist ((r * p),(r * q)) = dist (((r * p) - (r * p)),((r * p) - (r * q))) by Th25
.= dist (|[0,0]|,((r * p) - (r * q))) by EUCLID:54, RLVECT_1:5
.= dist (|[0,0]|,(r * (p - q))) by RLVECT_1:34
.= |.r.| * (dist (|[0,0]|,(p - q))) by Th20
.= |.r.| * (dist ((p - p),(p - q))) by EUCLID:54, RLVECT_1:5
.= |.r.| * (dist (p,q)) by Th25 ; :: thesis: verum