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

A1: now

assume J is automorphism ; :: thesis: ( ( for x, y being Scalar of K holds
( J . (x + y) = (J . x) + (J . y) & ( for x, y being Scalar of K holds
( J . (x * y) = (J . x) * (J . y) & J . (1_ K) = 1_ K ) ) ) ) & J is one-to-one & rng J = the carrier of K )
then A2: J is isomorphism by Def16;
then A3: J is monomorphism by Def12;
then J is linear by Def8;
then ( J is additive & J is multiplicative & J is unity-preserving ) by RINGCAT1:def 2;
hence for x, y being Scalar of K holds
( J . (x + y) = (J . x) + (J . y) & ( for x, y being Scalar of K holds
( J . (x * y) = (J . x) * (J . y) & J . (1_ K) = 1_ K ) ) ) by GRCAT_1:def 13, GROUP_1:def 17, GROUP_6:def 7; :: thesis: ( J is one-to-one & rng J = the carrier of K )
thus J is one-to-one by A3, Def8; :: thesis: rng J = the carrier of K
thus rng J = the carrier of K by A2, Def12; :: thesis: verum

end;

now

assume that
A4: ( ( for x, y being Scalar of K holds J . (x + y) = (J . x) + (J . y) ) & ( for x, y being Scalar of K holds J . (x * y) = (J . x) * (J . y) ) & J . (1_ K) = 1_ K ) and
A5: J is one-to-one and
A6: rng J = the carrier of K ; :: thesis: J is automorphism
( J is additive & J is multiplicative & J is unity-preserving ) by A4, GRCAT_1:def 13, GROUP_1:def 17, GROUP_6:def 7;
then J is linear by RINGCAT1:def 2;
then J is monomorphism by A5, Def8;
then J is isomorphism by A6, Def12;
hence J is automorphism by Def16; :: thesis: verum

end;

hence ( J is automorphism iff ( ( for x, y being Scalar of K holds J . (x + y) = (J . x) + (J . y) ) & ( for x, y being Scalar of K holds J . (x * y) = (J . x) * (J . y) ) & J . (1_ K) = 1_ K & J is one-to-one & rng J = the carrier of K ) ) by A1; :: thesis: verum