let R be Ring; :: thesis: for V being RightMod of R
for v being Vector of V holds v + ((Omega). V) = the carrier of V
let V be RightMod of R; :: thesis: for v being Vector of V holds v + ((Omega). V) = the carrier of V
let v be Vector of V; :: thesis: v + ((Omega). V) = the carrier of V
v in (Omega). V by RLVECT_1:3;
hence v + ((Omega). V) = the carrier of V by Lm3; :: thesis: verum