let G be strict Group; :: thesis: id the carrier of G is Element of Aut G
id the carrier of G is Homomorphism of G,G by GROUP_6:47;
then consider h being Homomorphism of G,G such that
A1: h = id the carrier of G ;
h is onto

proof

rng h = the carrier of G by A1, RELAT_1:71;
hence h is onto by FUNCT_2:def 3; :: thesis: verum

end;

hence id the carrier of G is Element of Aut G by A1, Def1; :: thesis: verum