theorem :: ZMODUL02:44

for V being Z_Module holds 0. (LC_Z_Module V) = ZeroLC V ;