:: deftheorem Def2 defines opp MOD_4:def 2 :
for K being non empty doubleLoopStr
for V being non empty ModuleStr over K
for b₃ being strict RightModStr over opp K holds
( b₃ = opp V iff for o being Function of [: the carrier of V, the carrier of (opp K):], the carrier of V st o = ~ the lmult of V holds
b₃ = RightModStr(# the carrier of V, the addF of V,(0. V),o #) );