let G be strict Group; :: thesis: for f being Element of Aut G holds f " is Element of Aut G
let f be Element of Aut G; :: thesis: f " is Element of Aut G
reconsider f = f as Homomorphism of G,G by Def1;
A1: f is bijective by Th5;
reconsider A = f " as Homomorphism of G,G by Th6;
A is bijective by A1, GROUP_6:73;
then A2: ( A is onto & A is one-to-one ) ;
thus f " is Element of Aut G by A2, Def1; :: thesis: verum