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