let p, q 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: |.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 RLVECT_1:def 8
.= dist (((r * q) + ((1 - r) * q)),((r * p) + ((1 - r) * q))) by RLVECT_1:def 6
.= dist ((r * q),(r * p)) by Th21
.= r * (dist (p,q)) by A1, Th26 ; :: thesis: verum