:: deftheorem defines antilinear MOD_4:def 7 :
for K, L being non empty doubleLoopStr
for IT being Function of K,L holds
( IT is antilinear iff ( IT is additive & IT is antimultiplicative & IT is unity-preserving ) );