let V be RealLinearSpace; :: thesis: for W being Subspace of V

for A being VECTOR of (VectQuot (V,W))

for v being VECTOR of V

for a being Real st A = v + W holds

- A = (- v) + W

let W be Subspace of V; :: thesis: for A being VECTOR of (VectQuot (V,W))

for v being VECTOR of V

for a being Real st A = v + W holds

- A = (- v) + W

let A be VECTOR of (VectQuot (V,W)); :: thesis: for v being VECTOR of V

for a being Real st A = v + W holds

- A = (- v) + W

let v be VECTOR of V; :: thesis: for a being Real st A = v + W holds

- A = (- v) + W

let a be Real; :: thesis: ( A = v + W implies - A = (- v) + W )

assume A1: A = v + W ; :: thesis: - A = (- v) + W

thus - A = (- 1) * A by RLVECT_1:16

.= ((- 1) * v) + W by A1, LMQ09

.= (- v) + W by RLVECT_1:16 ; :: thesis: verum

for A being VECTOR of (VectQuot (V,W))

for v being VECTOR of V

for a being Real st A = v + W holds

- A = (- v) + W

let W be Subspace of V; :: thesis: for A being VECTOR of (VectQuot (V,W))

for v being VECTOR of V

for a being Real st A = v + W holds

- A = (- v) + W

let A be VECTOR of (VectQuot (V,W)); :: thesis: for v being VECTOR of V

for a being Real st A = v + W holds

- A = (- v) + W

let v be VECTOR of V; :: thesis: for a being Real st A = v + W holds

- A = (- v) + W

let a be Real; :: thesis: ( A = v + W implies - A = (- v) + W )

assume A1: A = v + W ; :: thesis: - A = (- v) + W

thus - A = (- 1) * A by RLVECT_1:16

.= ((- 1) * v) + W by A1, LMQ09

.= (- v) + W by RLVECT_1:16 ; :: thesis: verum