theorem :: GROUP_24:45

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 ((incl1 (G,A,phi)) . g) |^ ((incl2 (G,A,phi)) . (a ")) = <*((phi . a) . g),(1_ A)*>