let E be RealNormSpace; :: thesis: for a, b being Point of E
for t being real number holds ((1 - t) * a) + (t * b) = a + (t * (b - a))
let a, b be Point of E; :: thesis: for t being real number holds ((1 - t) * a) + (t * b) = a + (t * (b - a))
let t be real number ; :: thesis: ((1 - t) * a) + (t * b) = a + (t * (b - a))
thus ((1 - t) * a) + (t * b) = ((1 * a) - (t * a)) + (t * b) by RLVECT_1:49
.= (a - (t * a)) + (t * b) by RLVECT_1:def 11
.= (a + (t * b)) - (t * a) by RLVECT_1:def 6
.= a + ((t * b) - (t * a)) by RLVECT_1:42
.= a + (t * (b - a)) by RLVECT_1:48 ; :: thesis: verum