let R be Ring; :: thesis: for V being RightMod of R
for v being Vector of V holds (ZeroLC V) . v = 0. R
let V be RightMod of R; :: thesis: for v being Vector of V holds (ZeroLC V) . v = 0. R
let v be Vector of V; :: thesis: (ZeroLC V) . v = 0. R
( Carrier (ZeroLC V) = {} & not v in {} ) by Def4;
hence (ZeroLC V) . v = 0. R ; :: thesis: verum