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

for A1, A2 being VECTOR of (VectQuot (V,W))

for v1, v2 being VECTOR of V st A1 = v1 + W & A2 = v2 + W holds

A1 - A2 = (v1 - v2) + W

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

for v1, v2 being VECTOR of V st A1 = v1 + W & A2 = v2 + W holds

A1 - A2 = (v1 - v2) + W

let A1, A2 be VECTOR of (VectQuot (V,W)); :: thesis: for v1, v2 being VECTOR of V st A1 = v1 + W & A2 = v2 + W holds

A1 - A2 = (v1 - v2) + W

let v1, v2 be VECTOR of V; :: thesis: ( A1 = v1 + W & A2 = v2 + W implies A1 - A2 = (v1 - v2) + W )

assume A1: ( A1 = v1 + W & A2 = v2 + W ) ; :: thesis: A1 - A2 = (v1 - v2) + W

then - A2 = (- v2) + W by LMQ10;

hence A1 - A2 = (v1 - v2) + W by A1, LMQ11; :: thesis: verum

for A1, A2 being VECTOR of (VectQuot (V,W))

for v1, v2 being VECTOR of V st A1 = v1 + W & A2 = v2 + W holds

A1 - A2 = (v1 - v2) + W

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

for v1, v2 being VECTOR of V st A1 = v1 + W & A2 = v2 + W holds

A1 - A2 = (v1 - v2) + W

let A1, A2 be VECTOR of (VectQuot (V,W)); :: thesis: for v1, v2 being VECTOR of V st A1 = v1 + W & A2 = v2 + W holds

A1 - A2 = (v1 - v2) + W

let v1, v2 be VECTOR of V; :: thesis: ( A1 = v1 + W & A2 = v2 + W implies A1 - A2 = (v1 - v2) + W )

assume A1: ( A1 = v1 + W & A2 = v2 + W ) ; :: thesis: A1 - A2 = (v1 - v2) + W

then - A2 = (- v2) + W by LMQ10;

hence A1 - A2 = (v1 - v2) + W by A1, LMQ11; :: thesis: verum