theorem Th18: :: GROUP_24:21

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for a1, a2 being Element of A
for g being Element of G holds (phi . a1) . ((phi . a2) . g) = (phi . (a1 * a2)) . g