theorem :: GROUP_24:43

for G, A being Group
for phi being Homomorphism of A,(AutGroup G) holds G, Image (incl1 (G,A,phi)) are_isomorphic by GROUP_6:68;