let p, q be Point of (TOP-REAL 2); :: thesis: for r being Real holds dist ((r * p),(r * q)) = (abs r) * (dist (p,q))
let r be Real; :: thesis: dist ((r * p),(r * q)) = (abs 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:42, EUCLID:54
.= dist (|[0,0]|,(r * (p - q))) by EUCLID:49
.= (abs r) * (dist (|[0,0]|,(p - q))) by Th20
.= (abs r) * (dist ((p - p),(p - q))) by EUCLID:42, EUCLID:54
.= (abs r) * (dist (p,q)) by Th25 ; :: thesis: verum