let K be Ring; :: thesis: for r being Scalar of K
for V being LeftMod of K
for a being Vector of V
for v being Vector of VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) st a = v holds
r * a = r * v
let r be Scalar of K; :: thesis: for V being LeftMod of K
for a being Vector of V
for v being Vector of VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) st a = v holds
r * a = r * v
let V be LeftMod of K; :: thesis: for a being Vector of V
for v being Vector of VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) st a = v holds
r * a = r * v
let a be Vector of V; :: thesis: for v being Vector of VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) st a = v holds
r * a = r * v
let v be Vector of VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #); :: thesis: ( a = v implies r * a = r * v )
assume A1: a = v ; :: thesis: r * a = r * v
thus r * a = the lmult of V . r,a by VECTSP_1:def 24
.= r * v by A1, VECTSP_1:def 24 ; :: thesis: verum