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
set X = RLSp2RVSp V;
set Y = RLSp2RVSp 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
reconsider x1 = v1, x2 = v2 as Vector of (RLSp2RVSp V) ;
reconsider B1 = A1, B2 = A2 as Vector of (VectQuot ((RLSp2RVSp V),(RLSp2RVSp W))) ;
A2: ( B1 = x1 + (RLSp2RVSp W) & B2 = x2 + (RLSp2RVSp W) ) by A1, LMQ03;
thus A1 + A2 = B1 + B2
.= (x1 + x2) + (RLSp2RVSp W) by A2, VECTSP10:26
.= (v1 + v2) + W by LMQ03 ; :: thesis: verum