let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n)
for r being real number holds (((1 - r) * p) + (r * q)) - p = r * (q - p)
let p, q be Point of (TOP-REAL n); :: thesis: for r being real number holds (((1 - r) * p) + (r * q)) - p = r * (q - p)
let r be real number ; :: thesis: (((1 - r) * p) + (r * q)) - p = r * (q - p)
A1: n in NAT by ORDINAL1:def 12;
thus (((1 - r) * p) + (r * q)) - p = (r * q) + (((1 - r) * p) - p) by EUCLID:45
.= (r * q) + (((1 * p) - (r * p)) - p) by EUCLID:50
.= (r * q) + ((p - (r * p)) - p) by RLVECT_1:def 8
.= (r * q) + ((p - p) - (r * p)) by A1, TOPREAL9:1
.= (r * q) + ((0. (TOP-REAL n)) - (r * p)) by RLVECT_1:15
.= (r * q) - (r * p) by RLVECT_1:14
.= r * (q - p) by EUCLID:49 ; :: thesis: verum