theorem Th14: :: AUTGROUP:14

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