let p, q be Point of (TOP-REAL 2); for r being Real st 0 <= r holds
dist (q,((r * p) + ((1 - r) * q))) = r * (dist (p,q))
let r be Real; ( 0 <= r implies dist (q,((r * p) + ((1 - r) * q))) = r * (dist (p,q)) )
assume
0 <= r
; 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
; verum