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