let V be Z_Module; :: thesis: for v being Element of V holds (ZeroLC V) . v = 0. INT.Ring
let v be Element of V; :: thesis: (ZeroLC V) . v = 0. INT.Ring
( Carrier (ZeroLC V) = {} & not v in {} ) by VECTSP_6:def 3;
hence (ZeroLC V) . v = 0. INT.Ring ; :: thesis: verum