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;

reconsider A = f " as Homomorphism of G,G by Th5;

f is bijective by Th4;

then A is bijective by GROUP_6:63;

hence f " is Element of Aut G by Def1; :: thesis: verum

let f be Element of Aut G; :: thesis: f " is Element of Aut G

reconsider f = f as Homomorphism of G,G by Def1;

reconsider A = f " as Homomorphism of G,G by Th5;

f is bijective by Th4;

then A is bijective by GROUP_6:63;

hence f " is Element of Aut G by Def1; :: thesis: verum