:: deftheorem defines LC_Z_Module ZMODUL02:def 34 :
for R being Ring
for V being LeftMod of R holds LC_Z_Module V = ModuleStr(# (LinComb V),(LCAdd V),(@ (ZeroLC V)),(LCMult V) #);