let V be RealLinearSpace; :: thesis: for u, v, y being VECTOR of V holds
( (u - y) - (v - y) = u - v & (u + y) - (v + y) = u - v )
let u, v, y be VECTOR of V; :: thesis: ( (u - y) - (v - y) = u - v & (u + y) - (v + y) = u - v )
thus (u - y) - (v - y) = (u - y) + (y - v) by RLVECT_1:33
.= u - v by ANALOAF:1 ; :: thesis: (u + y) - (v + y) = u - v
thus (u + y) - (v + y) = (u - (- y)) - (v + y) by RLVECT_1:17
.= (u - (- y)) - (v - (- y)) by RLVECT_1:17
.= (u - (- y)) + ((- y) - v) by RLVECT_1:33
.= u - v by ANALOAF:1 ; :: thesis: verum