let K be Ring; :: thesis: for r being Scalar of
for V being LeftMod of
for a being Vector of
for v being Vector of st a = v holds
r * a = r * v
let r be Scalar of ; :: thesis: for V being LeftMod of
for a being Vector of
for v being Vector of st a = v holds
r * a = r * v
let V be LeftMod of ; :: thesis: for a being Vector of
for v being Vector of st a = v holds
r * a = r * v
let a be Vector of ; :: thesis: for v being Vector of st a = v holds
r * a = r * v
let v be Vector of ; :: 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