let V be Z_Module; :: 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 Th24, RLVECT_1:1;
hence w is VECTOR of V ; :: thesis: verum