theorem :: MOD_4:38

for K being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr
for J being Function of K,K holds
( J is isomorphism iff opp J is antiisomorphism ) by Th29;