let K be non empty doubleLoopStr ; :: thesis: id K is automorphism
set J = id K;
A1: id K is monomorphism

proof

A2: id K is linear

proof

( ( for x, y being Scalar of K holds (id K) . (x + y) = ((id K) . x) + ((id K) . y) ) & ( for x, y being Scalar of K holds (id K) . (x * y) = ((id K) . x) * ((id K) . y) ) & (id K) . (1_ K) = 1_ K ) by Lm6;
then ( id K is additive & id K is multiplicative & id K is unity-preserving ) by GRCAT_1:def 13, GROUP_1:def 17, GROUP_6:def 7;
hence id K is linear by RINGCAT1:def 2; :: thesis: verum

end;

id K is one-to-one by Lm6;
hence id K is monomorphism by A2, Def8; :: thesis: verum

end;

rng (id K) = the carrier of K by Lm6;
then id K is isomorphism by A1, Def12;
hence id K is automorphism by Def16; :: thesis: verum