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:46, EUCLID:58
.= dist |[0 ,0 ]|,(r * (p - q)) by EUCLID:53
.= (abs r) * (dist |[0 ,0 ]|,(p - q)) by Th20
.= (abs r) * (dist (p - p),(p - q)) by EUCLID:46, EUCLID:58
.= (abs r) * (dist p,q) by Th25 ; :: thesis: verum