let K be non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr ; :: thesis: for J being Function of K,K holds
( J is automorphism iff opp J is antiisomorphism )
let J be Function of K,K; :: thesis: ( J is automorphism iff opp J is antiisomorphism )
( J is isomorphism iff opp J is antiisomorphism ) by Th41;
hence ( J is automorphism iff opp J is antiisomorphism ) by Def16; :: thesis: verum