let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G)
for a1, a2 being Element of A
for g being Element of G holds (phi . a1) . ((phi . a2) . g) = (phi . (a1 * a2)) . g
let phi be Homomorphism of A,(AutGroup G); :: thesis: for a1, a2 being Element of A
for g being Element of G holds (phi . a1) . ((phi . a2) . g) = (phi . (a1 * a2)) . g
let a1, a2 be Element of A; :: thesis: for g being Element of G holds (phi . a1) . ((phi . a2) . g) = (phi . (a1 * a2)) . g
let g be Element of G; :: thesis: (phi . a1) . ((phi . a2) . g) = (phi . (a1 * a2)) . g
reconsider phi1 = phi . a1, phi2 = phi . a2 as Homomorphism of G,G by AUTGROUP:def 1;
phi . (a1 * a2) = (phi . a1) * (phi . a2) by GROUP_6:def 6;
then (phi . (a1 * a2)) . g = (phi1 * phi2) . g by AUTGROUP:8
.= phi1 . (phi2 . g) by FUNCT_2:15 ;
hence (phi . a1) . ((phi . a2) . g) = (phi . (a1 * a2)) . g ; :: thesis: verum