for G being strict Group
for f, g being Element of InnAut G holds (AutComp G) . (f,g) = f * g