let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G)
for a being Element of A
for g being Element of G holds
( (phi . (a ")) . ((phi . a) . g) = g & (phi . a) . ((phi . (a ")) . g) = g )
let phi be Homomorphism of A,(AutGroup G); :: thesis: for a being Element of A
for g being Element of G holds
( (phi . (a ")) . ((phi . a) . g) = g & (phi . a) . ((phi . (a ")) . g) = g )
let a be Element of A; :: thesis: for g being Element of G holds
( (phi . (a ")) . ((phi . a) . g) = g & (phi . a) . ((phi . (a ")) . g) = g )
let g be Element of G; :: thesis: ( (phi . (a ")) . ((phi . a) . g) = g & (phi . a) . ((phi . (a ")) . g) = g )
thus (phi . (a ")) . ((phi . a) . g) = (phi . ((a ") * a)) . g by Th18
.= (phi . (1_ A)) . g by GROUP_1:def 5
.= g by Th15 ; :: thesis: (phi . a) . ((phi . (a ")) . g) = g
thus (phi . a) . ((phi . (a ")) . g) = (phi . (a * (a "))) . g by Th18
.= (phi . (1_ A)) . g by GROUP_1:def 5
.= g by Th15 ; :: thesis: verum