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

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