let R be Ring; :: thesis: for V being RightMod of
for W being Submodule of V
for w being Vector of holds w is Vector of
let V be RightMod of ; :: thesis: for W being Submodule of V
for w being Vector of holds w is Vector of
let W be Submodule of V; :: thesis: for w being Vector of holds w is Vector of
let w be Vector of ; :: thesis: w is Vector of
w in V by Th17, RLVECT_1:3;
hence w is Vector of by STRUCT_0:def 5; :: thesis: verum