let q, p be Point of (TOP-REAL 2); :: thesis: for r being Real st 0 <= r holds
dist (q,((r * p) + ((1 - r) * q))) = r * (dist (p,q))
let r be Real; :: thesis: ( 0 <= r implies dist (q,((r * p) + ((1 - r) * q))) = r * (dist (p,q)) )
assume 0 <= r ; :: thesis: dist (q,((r * p) + ((1 - r) * q))) = r * (dist (p,q))
then A1: abs r = r by ABSVALUE:def 1;
thus dist (q,((r * p) + ((1 - r) * q))) = dist (((r * p) + ((1 - r) * q)),((r + (1 - r)) * q)) by EUCLID:33
.= dist (((r * q) + ((1 - r) * q)),((r * p) + ((1 - r) * q))) by EUCLID:37
.= dist ((r * q),(r * p)) by Th21
.= r * (dist (p,q)) by A1, Th26 ; :: thesis: verum