let G be strict Group; :: thesis: for f1, f2 being Element of Aut G holds f1 * f2 is Element of Aut G
let f1, f2 be Element of Aut G; :: thesis: f1 * f2 is Element of Aut G
reconsider f1 = f1, f2 = f2 as Homomorphism of G,G by Def1;
( f1 is bijective & f2 is bijective ) by Th4;
then f1 * f2 is bijective ;
hence f1 * f2 is Element of Aut G by Th4; :: thesis: verum