let E be RealNormSpace; :: thesis: for a, b being Point of E
for t being Real holds ((1 - t) * a) + (t * b) = a + (t * (b - a))
let a, b be Point of E; :: thesis: for t being Real holds ((1 - t) * a) + (t * b) = a + (t * (b - a))
let t be Real; :: 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:35
.= (a - (t * a)) + (t * b) by RLVECT_1:def 8
.= (a + (t * b)) - (t * a) by RLVECT_1:def 3
.= a + ((t * b) - (t * a)) by RLVECT_1:28
.= a + (t * (b - a)) by RLVECT_1:34 ; :: thesis: verum