let V be RealLinearSpace; :: thesis: for v1, v2, w, y being VECTOR of V
for b1, b2, c1, c2 being Real st v1 = (b1 * w) + (b2 * y) & v2 = (c1 * w) + (c2 * y) holds
( v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) )
let v1, v2, w, y be VECTOR of V; :: thesis: for b1, b2, c1, c2 being Real st v1 = (b1 * w) + (b2 * y) & v2 = (c1 * w) + (c2 * y) holds
( v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) )
let b1, b2, c1, c2 be Real; :: thesis: ( v1 = (b1 * w) + (b2 * y) & v2 = (c1 * w) + (c2 * y) implies ( v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) ) )
assume A1: ( v1 = (b1 * w) + (b2 * y) & v2 = (c1 * w) + (c2 * y) ) ; :: thesis: ( v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) )
hence v1 + v2 = (((b1 * w) + (b2 * y)) + (c1 * w)) + (c2 * y) by RLVECT_1:def 3
.= (((b1 * w) + (c1 * w)) + (b2 * y)) + (c2 * y) by RLVECT_1:def 3
.= (((b1 + c1) * w) + (b2 * y)) + (c2 * y) by RLVECT_1:def 6
.= ((b1 + c1) * w) + ((b2 * y) + (c2 * y)) by RLVECT_1:def 3
.= ((b1 + c1) * w) + ((b2 + c2) * y) by RLVECT_1:def 6 ;
:: thesis: v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y)
thus v1 - v2 = ((b1 * w) + (b2 * y)) + ((- (c1 * w)) + (- (c2 * y))) by A1, RLVECT_1:31
.= ((b1 * w) + (b2 * y)) + ((c1 * (- w)) + (- (c2 * y))) by RLVECT_1:25
.= ((b1 * w) + (b2 * y)) + ((c1 * (- w)) + (c2 * (- y))) by RLVECT_1:25
.= ((b1 * w) + (b2 * y)) + (((- c1) * w) + (c2 * (- y))) by RLVECT_1:24
.= ((b1 * w) + (b2 * y)) + (((- c1) * w) + ((- c2) * y)) by RLVECT_1:24
.= (((b1 * w) + (b2 * y)) + ((- c1) * w)) + ((- c2) * y) by RLVECT_1:def 3
.= (((b1 * w) + ((- c1) * w)) + (b2 * y)) + ((- c2) * y) by RLVECT_1:def 3
.= (((b1 + (- c1)) * w) + (b2 * y)) + ((- c2) * y) by RLVECT_1:def 6
.= ((b1 + (- c1)) * w) + ((b2 * y) + ((- c2) * y)) by RLVECT_1:def 3
.= ((b1 - c1) * w) + ((b2 + (- c2)) * y) by RLVECT_1:def 6
.= ((b1 - c1) * w) + ((b2 - c2) * y) ; :: thesis: verum