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