theorem :: AUTGROUP:8

for G being Group
for x, y being Element of (AutGroup G)
for f, g being Element of Aut G st x = f & y = g holds
x * y = f * g by Def2;