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 antiepimorphism iff opp J is epimorphism )
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 antiepimorphism iff opp J is epimorphism )
let J be Function of K,L; :: thesis: ( J is antiepimorphism iff opp J is epimorphism )
set J' = opp J;
set L' = opp L;
A1: ( rng J = the carrier of L iff rng (opp J) = the carrier of (opp L) ) ;
( J is antilinear iff opp J is linear ) by Th36;
hence ( J is antiepimorphism iff opp J is epimorphism ) by A1, Def10, Def11; :: thesis: verum