let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive 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 Th23;
then A2: A2 in { B where B is Coset of W : verum } ;
A1 is Coset of W by Th23;
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