:: deftheorem defines TrivialLMod MOD_2:def 1 :
for R being Ring holds TrivialLMod R = ModuleStr(# {0},op2,op0,(pr2 ( the carrier of R,{0})) #);