let R be Ring; :: thesis: for V being LeftMod of R

for v being Element of V holds (ZeroLC V) . v = 0. R

let V be LeftMod of R; :: thesis: for v being Element of V holds (ZeroLC V) . v = 0. R

let v be Element of V; :: thesis: (ZeroLC V) . v = 0. R

( Carrier (ZeroLC V) = {} & not v in {} ) by VECTSP_6:def 3;

hence (ZeroLC V) . v = 0. R ; :: thesis: verum

for v being Element of V holds (ZeroLC V) . v = 0. R

let V be LeftMod of R; :: thesis: for v being Element of V holds (ZeroLC V) . v = 0. R

let v be Element of V; :: thesis: (ZeroLC V) . v = 0. R

( Carrier (ZeroLC V) = {} & not v in {} ) by VECTSP_6:def 3;

hence (ZeroLC V) . v = 0. R ; :: thesis: verum