let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G)
for g being Element of G holds (phi . (1_ A)) . g = g
let phi be Homomorphism of A,(AutGroup G); :: thesis: for g being Element of G holds (phi . (1_ A)) . g = g
let g be Element of G; :: thesis: (phi . (1_ A)) . g = g
phi . (1_ A) = 1_ (AutGroup G) by GROUP_6:31
.= id the carrier of G by AUTGROUP:9 ;
hence (phi . (1_ A)) . g = g ; :: thesis: verum