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 ModuleStr(# the carrier of V, the addF of V, the ZeroF 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 ModuleStr(# the carrier of V, the addF of V, the ZeroF 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 ModuleStr(# the carrier of V, the addF of V, the ZeroF 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 ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) st a = v holds
r * a = r * v
let v be Vector of ModuleStr(# the carrier of V, the addF of V, the ZeroF 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 12
.= r * v by A1, VECTSP_1:def 12 ; :: thesis: verum