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