reconsider i = id the carrier of G as Automorphism of G by GROUP_6:38;
take i ; :: thesis: i is inner
take 1_ G ; :: according to GROUP_22:def 3 :: thesis: 1_ G is_inner_wrt i
thus 1_ G is_inner_wrt i by GROUP_3:19; :: thesis: verum