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 A being Vector of (VectQuot (V,W))
for v being Vector of V
for a being Scalar of st A = v + W holds
a * A = (a * v) + W
let V be VectSp of K; :: thesis: for W being Subspace of V
for A being Vector of (VectQuot (V,W))
for v being Vector of V
for a being Scalar of st A = v + W holds
a * A = (a * v) + W
let W be Subspace of V; :: thesis: for A being Vector of (VectQuot (V,W))
for v being Vector of V
for a being Scalar of st A = v + W holds
a * A = (a * v) + W
set vw = VectQuot (V,W);
set lm = the lmult of (VectQuot (V,W));
let A be Vector of (VectQuot (V,W)); :: thesis: for v being Vector of V
for a being Scalar of st A = v + W holds
a * A = (a * v) + W
let v be Vector of V; :: thesis: for a being Scalar of st A = v + W holds
a * A = (a * v) + W
let a be Scalar of ; :: thesis: ( A = v + W implies a * A = (a * v) + W )
assume A1: A = v + W ; :: thesis: a * A = (a * v) + W
A is Coset of W by Th22;
then A in { B where B is Coset of W : verum } ;
then reconsider w = A as Element of CosetSet (V,W) ;
thus a * A = the lmult of (VectQuot (V,W)) . (a,A)
.= (lmultCoset (V,W)) . (a,w) by Def6
.= (a * v) + W by A1, Def5 ; :: thesis: verum