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 antimonomorphism iff opp J is monomorphism )
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 antimonomorphism iff opp J is monomorphism )
let J be Function of K,L; :: thesis: ( J is antimonomorphism iff opp J is monomorphism )
set J9 = opp J;
A1: ( J is antilinear iff opp J is linear ) by Th36;
( opp J is monomorphism iff ( opp J is linear & opp J is one-to-one ) ) by Def8;
hence ( J is antimonomorphism iff opp J is monomorphism ) by A1, Def9; :: thesis: verum