theorem :: ZMODUL02:45

for V being Z_Module holds the addF of (LC_Z_Module V) = LCAdd V ;