let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n)
for r being Real holds ((1 - r) * p) + (r * q) = p + (r * (q - p))
let p, q be Point of (TOP-REAL n); :: thesis: for r being Real holds ((1 - r) * p) + (r * q) = p + (r * (q - p))
let r be Real; :: thesis: ((1 - r) * p) + (r * q) = p + (r * (q - p))
thus p + (r * (q - p)) = ((((1 - r) * p) + (r * q)) - p) + p by Lm1
.= (((1 - r) * p) + (r * q)) - (p - p) by RLVECT_1:29
.= (((1 - r) * p) + (r * q)) - (0. (TOP-REAL n)) by RLVECT_1:15
.= ((1 - r) * p) + (r * q) ; :: thesis: verum