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

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