set f = id G;
for x, y being Element of G holds (id G) . (x + y) = ((id G) . x) + ((id G) . y) by Lm14;
then reconsider f = id G as Homomorphism of G,G by Def19;
( f is one-to-one & f is onto ) by Lm14;
hence id G is Automorphism of G by FUNCT_2:def 4; :: thesis: verum