let R be Ring; :: thesis: for a being Scalar of R
for V being RightMod of R
for v being Vector of V
for W being Submodule of V
for w being Vector of W st w = v holds
w * a = v * a
let a be Scalar of R; :: thesis: for V being RightMod of R
for v being Vector of V
for W being Submodule of V
for w being Vector of W st w = v holds
w * a = v * a
let V be RightMod of R; :: thesis: for v being Vector of V
for W being Submodule of V
for w being Vector of W st w = v holds
w * a = v * a
let v be Vector of V; :: thesis: for W being Submodule of V
for w being Vector of W st w = v holds
w * a = v * a
let W be Submodule of V; :: thesis: for w being Vector of W st w = v holds
w * a = v * a
let w be Vector of W; :: thesis: ( w = v implies w * a = v * a )
assume A1: w = v ; :: thesis: w * a = v * a
w * a = ( the rmult of V | [: the carrier of W, the carrier of R:]) . [w,a] by Def2;
hence w * a = v * a by A1, FUNCT_1:49; :: thesis: verum