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;

A1: f is bijective by Th4;

then dom f = the carrier of G by GROUP_6:61;

hence ( dom f = rng f & dom f = the carrier of G ) by A1, GROUP_6:61; :: thesis: verum

( 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;

A1: f is bijective by Th4;

then dom f = the carrier of G by GROUP_6:61;

hence ( dom f = rng f & dom f = the carrier of G ) by A1, GROUP_6:61; :: thesis: verum