let K be Ring; 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; 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; 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; 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 #); ( a = v implies r * a = r * v )
assume A1:
a = v
; 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
; verum