let G be strict Group; :: thesis: id the carrier of G = 1_ (AutGroup G)
consider f being Element of (AutGroup G);
reconsider g = id the carrier of G as Element of (AutGroup G) by Th4;
consider g1 being Function of the carrier of G,the carrier of G such that
A1: g1 = g ;
f is Homomorphism of G,G by Def1;
then consider f1 being Function of the carrier of G,the carrier of G such that
A2: f1 = f ;
( f1 = f & g1 = g implies f1 * g1 = f * g ) by Def2;
hence id the carrier of G = 1_ (AutGroup G) by A1, A2, FUNCT_2:23, GROUP_1:15; :: thesis: verum