theorem Th18: :: AUTGROUP:18

for G being Group
for x, y being Element of (InnAutGroup G)
for f, g being Element of InnAut G st x = f & y = g holds
x * y = f * g