let V be RealLinearSpace; :: thesis: for u, w being VECTOR of V ex y being VECTOR of V st u # y = w
let u, w be VECTOR of V; :: thesis: ex y being VECTOR of V st u # y = w
take y = (- u) + (w + w); :: thesis: u # y = w
u + y = (u + (- u)) + (w + w) by RLVECT_1:def 3
.= (0. V) + (w + w) by RLVECT_1:5
.= w + w by RLVECT_1:4 ;
hence u # y = w by Def2; :: thesis: verum