let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for L being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr
for J being Function of K,L holds
( J is isomorphism iff opp J is antiisomorphism )
let L be non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr ; :: thesis: for J being Function of K,L holds
( J is isomorphism iff opp J is antiisomorphism )
let J be Function of K,L; :: thesis: ( J is isomorphism iff opp J is antiisomorphism )
set J9 = opp J;
set L9 = opp L;
A1: ( J is onto iff opp J is onto ) ;
( J is monomorphism iff opp J is antimonomorphism ) by Th37;
hence ( J is isomorphism iff opp J is antiisomorphism ) by A1, Def12, Def13; :: thesis: verum