theorem Th36: :: GROUP_24:44

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)*>