theorem Th22: :: MOD_4:22

for K being non empty doubleLoopStr
for J being Function of K,K holds
( J is antiisomorphism iff ( J is additive & ( for x, y being Scalar of K holds J . (x * y) = (J . y) * (J . x) ) & J . (1_ K) = 1_ K & J is one-to-one & J is onto ) )