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

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