let V be RealLinearSpace; :: thesis: for u2, v, u1 being VECTOR of V
for a2, a1 being Real holds (u2 + (a2 * v)) - (u1 + (a1 * v)) = (u2 - u1) + ((a2 - a1) * v)
let u2, v, u1 be VECTOR of V; :: thesis: for a2, a1 being Real holds (u2 + (a2 * v)) - (u1 + (a1 * v)) = (u2 - u1) + ((a2 - a1) * v)
let a2, a1 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:41
.= ((a2 * v) + (u2 - u1)) - (a1 * v) by RLVECT_1:def 6
.= (u2 - u1) + ((a2 * v) - (a1 * v)) by RLVECT_1:def 6
.= (u2 - u1) + ((a2 - a1) * v) by RLVECT_1:49 ; :: thesis: verum