let G be strict Group; :: thesis: for f being Element of Aut G holds
( dom f = rng f & dom f = the carrier of G )
let f be Element of Aut G; :: thesis: ( dom f = rng f & dom f = the carrier of G )
reconsider f = f as Homomorphism of G,G by Def1;
f is bijective by Th5;
then ( dom f = the carrier of G & rng f = the carrier of G ) by GROUP_6:71;
hence ( dom f = rng f & dom f = the carrier of G ) ; :: thesis: verum