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 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 Th23;
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 by VECTSP_1:def 24
.= (lmultCoset V,W) . a,w by Def6
.= (a * v) + W by A1, Def5 ; :: thesis: verum