let G be strict Group; :: thesis: id the carrier of G = 1_ (AutGroup G)
set f = the Element of (AutGroup G);
reconsider g = id the carrier of G as Element of (AutGroup G) by Th3;
consider g1 being Function of the carrier of G, the carrier of G such that
A1: g1 = g ;
the Element of (AutGroup G) 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 = the Element of (AutGroup G) ;
( f1 = the Element of (AutGroup G) & g1 = g implies f1 * g1 = the Element of (AutGroup G) * g ) by Def2;
hence id the carrier of G = 1_ (AutGroup G) by A1, A2, FUNCT_2:17, GROUP_1:7; :: thesis: verum