let V be RealLinearSpace; :: thesis: for u, v, y being VECTOR of V holds (u - y) - (v - y) = u - v
let u, v, y be VECTOR of V; :: thesis: (u - y) - (v - y) = u - v
thus (u - y) - (v - y) = u - ((v - y) + y) by RLVECT_1:27
.= u - v by RLSUB_2:61 ; :: thesis: verum