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