let G be strict Group; :: thesis: for f, g being Element of InnAut G holds (AutComp G) . (f,g) = f * g
let f, g be Element of InnAut G; :: thesis: (AutComp G) . (f,g) = f * g
( f is Element of Aut G & g is Element of Aut G ) by Th12;
hence (AutComp G) . (f,g) = f * g by Def2; :: thesis: verum