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