let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for a, b, c, d being Real holds ((a * w) + (b * y)) - ((c * w) + (d * y)) = ((a - c) * w) + ((b - d) * y)
let w, y be VECTOR of V; :: thesis: for a, b, c, d being Real holds ((a * w) + (b * y)) - ((c * w) + (d * y)) = ((a - c) * w) + ((b - d) * y)
let a, b, c, d be Real; :: thesis: ((a * w) + (b * y)) - ((c * w) + (d * y)) = ((a - c) * w) + ((b - d) * y)
thus ((a * w) + (b * y)) - ((c * w) + (d * y)) = (b * y) + ((a * w) - ((c * w) + (d * y))) by RLVECT_1:def 3
.= (b * y) + (((a * w) - (c * w)) - (d * y)) by RLVECT_1:27
.= (b * y) + (((a - c) * w) - (d * y)) by RLVECT_1:35
.= (((a - c) * w) + (b * y)) - (d * y) by RLVECT_1:def 3
.= ((a - c) * w) + ((b * y) - (d * y)) by RLVECT_1:def 3
.= ((a - c) * w) + ((b - d) * y) by RLVECT_1:35 ; :: thesis: verum