theorem Th19: :: GROUP_24:22

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for a being Element of A
for g being Element of G holds
( (phi . (a ")) . ((phi . a) . g) = g & (phi . a) . ((phi . (a ")) . g) = g )