let R be Ring; :: thesis: for V being RightMod of
for v being Vector of holds v + ((Omega). V) = the carrier of V
let V be RightMod of ; :: thesis: for v being Vector of holds v + ((Omega). V) = the carrier of V
let v be Vector of ; :: 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