let K be non empty doubleLoopStr ; :: thesis: for J being Function of K,K holds
( J is antiisomorphism iff ( J is additive & ( for x, y being Scalar of K holds J . (x * y) = (J . y) * (J . x) ) & J . (1_ K) = 1_ K & J is one-to-one & J is onto ) )
let J be Function of K,K; :: thesis: ( J is antiisomorphism iff ( J is additive & ( for x, y being Scalar of K holds J . (x * y) = (J . y) * (J . x) ) & J . (1_ K) = 1_ K & J is one-to-one & J is onto ) )

A1: now

assume A2: J is antiisomorphism ; :: thesis: ( J is additive & ( for x, y being Scalar of K holds
( J . (x * y) = (J . y) * (J . x) & J . (1_ K) = 1_ K ) ) & J is one-to-one & J is onto )
then A3: J is antimonomorphism by Def13;
then J is antilinear by Def9;
hence ( J is additive & ( for x, y being Scalar of K holds
( J . (x * y) = (J . y) * (J . x) & J . (1_ K) = 1_ K ) ) ) by Def6, GROUP_1:def 13; :: thesis: ( J is one-to-one & J is onto )
thus J is one-to-one by A3, Def9; :: thesis: J is onto
thus J is onto by A2, Def13; :: thesis: verum

end;

now

assume that
A4: ( J is additive & ( for x, y being Scalar of K holds J . (x * y) = (J . y) * (J . x) ) & J . (1_ K) = 1_ K ) and
A5: J is one-to-one and
A6: J is onto ; :: thesis: J is antiisomorphism
( J is additive & J is antimultiplicative & J is unity-preserving ) by A4, Def6, GROUP_1:def 13;
then J is antimonomorphism by A5, Def9;
hence J is antiisomorphism by A6, Def13; :: thesis: verum

end;

hence ( J is antiisomorphism iff ( J is additive & ( for x, y being Scalar of K holds J . (x * y) = (J . y) * (J . x) ) & J . (1_ K) = 1_ K & J is one-to-one & J is onto ) ) by A1; :: thesis: verum