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