:: deftheorem defines opp MOD_4:def 16 :
for K, L being non empty doubleLoopStr
for J being Function of K,L holds opp J = J;