let R be Ring; :: thesis: for V being RightMod of R
for v being Vector of V
for W being Submodule of V
for w being Vector of W st w = v holds
- v = - w
let V be RightMod of R; :: thesis: for v being Vector of V
for W being Submodule of V
for w being Vector of W st w = v holds
- v = - w
let v be Vector of V; :: thesis: for W being Submodule of V
for w being Vector of W st w = v holds
- v = - w
let W be Submodule of V; :: thesis: for w being Vector of W st w = v holds
- v = - w
let w be Vector of W; :: thesis: ( w = v implies - v = - w )
A1: ( - v = v * (- (1_ R)) & - w = w * (- (1_ R)) ) by VECTSP_2:32;
assume w = v ; :: thesis: - v = - w
hence - v = - w by A1, Th14; :: thesis: verum