let G be strict Group; :: thesis: for f being Element of Aut G holds f " is Homomorphism of G,G
let f be Element of Aut G; :: thesis: f " is Homomorphism of G,G
reconsider f = f as Homomorphism of G,G by Def1;
f is bijective by Th5;
hence f " is Homomorphism of G,G by GROUP_6:72; :: thesis: verum