let K be non empty doubleLoopStr ; :: thesis: id K is automorphism
set J = id K;
A1: (id K) . (1_ K) = 1_ K by Lm6;
( ( 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) ) ) by Lm6;
then ( id K is additive & id K is multiplicative & id K is unity-preserving ) by A1, GRCAT_1:def 13, GROUP_1:def 17, GROUP_6:def 7;
then A2: id K is linear by RINGCAT1:def 2;
A3: rng (id K) = the carrier of K by Lm6;
id K is one-to-one by Lm6;
then id K is monomorphism by A2, Def8;
then id K is isomorphism by A3, Def12;
hence id K is automorphism by Def16; :: thesis: verum