:: deftheorem defines opp MOD_4:def 5 :
for K being non empty doubleLoopStr
for W being non empty RightModStr over K
for o being Function of [: the carrier of W, the carrier of K:], the carrier of W holds opp o = ~ o;