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:38;

then consider h being Homomorphism of G,G such that

A1: h = id the carrier of G ;

rng h = the carrier of G by A1, RELAT_1:45;

then h is onto ;

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

id the carrier of G is Homomorphism of G,G by GROUP_6:38;

then consider h being Homomorphism of G,G such that

A1: h = id the carrier of G ;

rng h = the carrier of G by A1, RELAT_1:45;

then h is onto ;

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