theorem Th17: :: AUTGROUP:17

for G being Group
for f, g being Element of InnAut G holds f * g is Element of InnAut G