let V be RealLinearSpace; :: thesis: for u1, u2, v being VECTOR of V
for a1, a2 being Real holds (u2 + (a2 * v)) - (u1 + (a1 * v)) = (u2 - u1) + ((a2 - a1) * v)
let u1, u2, v be VECTOR of V; :: thesis: for a1, a2 being Real holds (u2 + (a2 * v)) - (u1 + (a1 * v)) = (u2 - u1) + ((a2 - a1) * v)
let a1, a2 be Real; :: thesis: (u2 + (a2 * v)) - (u1 + (a1 * v)) = (u2 - u1) + ((a2 - a1) * v)
thus (u2 + (a2 * v)) - (u1 + (a1 * v)) = ((u2 + (a2 * v)) - u1) - (a1 * v) by RLVECT_1:27
.= ((a2 * v) + (u2 - u1)) - (a1 * v) by RLVECT_1:def 3
.= (u2 - u1) + ((a2 * v) - (a1 * v)) by RLVECT_1:def 3
.= (u2 - u1) + ((a2 - a1) * v) by RLVECT_1:35 ; :: thesis: verum