let G be 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