theorem Th7: :: AUTGROUP:7

for G being Group
for f1, f2 being Element of Aut G holds f1 * f2 is Element of Aut G