let V be RealUnitarySpace; :: thesis: for W being Subspace of V
for v being VECTOR of V
for w being VECTOR of W st w = v holds
- v = - w
let W be Subspace of V; :: thesis: for v being VECTOR of V
for w being VECTOR of W st w = v holds
- v = - w
let v be VECTOR 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 = (- 1) * v & - w = (- 1) * w ) by RLVECT_1:16;
assume w = v ; :: thesis: - v = - w
hence - v = - w by A1, Th7; :: thesis: verum