let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for V being VectSp of K
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 V be VectSp of K; :: 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 vw = VectQuot (V,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
A2 is Coset of W by Th22;
then A2: A2 in { B where B is Coset of W : verum } ;
A1 is Coset of W by Th22;
then A1 in { B where B is Coset of W : verum } ;
then reconsider w1 = A1, w2 = A2 as Element of CosetSet (V,W) by A2;
thus A1 + A2 = (addCoset (V,W)) . (w1,w2) by Def6
.= (v1 + v2) + W by A1, Def3 ; :: thesis: verum