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

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