let G be strict Group; :: thesis: id the carrier of G = 1_ (InnAutGroup G)

id the carrier of G = 1_ (AutGroup G) by Th9;

hence id the carrier of G = 1_ (InnAutGroup G) by GROUP_2:44; :: thesis: verum

id the carrier of G = 1_ (AutGroup G) by Th9;

hence id the carrier of G = 1_ (InnAutGroup G) by GROUP_2:44; :: thesis: verum