let R be Ring; :: thesis: for V being RightMod of R
for W being Submodule of V
for w being Vector of W holds w is Vector of V
let V be RightMod of R; :: thesis: for W being Submodule of V
for w being Vector of W holds w is Vector of V
let W be Submodule of V; :: thesis: for w being Vector of W holds w is Vector of V
let w be Vector of W; :: thesis: w is Vector of V
w in V by Th9, RLVECT_1:1;
hence w is Vector of V ; :: thesis: verum