let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G)
for g being Element of G
for x being Element of (semidirect_product (G,A,phi)) st x = <*g,(1_ A)*> holds
x " = <*(g "),(1_ A)*>
let phi be Homomorphism of A,(AutGroup G); :: thesis: for g being Element of G
for x being Element of (semidirect_product (G,A,phi)) st x = <*g,(1_ A)*> holds
x " = <*(g "),(1_ A)*>
let g be Element of G; :: thesis: for x being Element of (semidirect_product (G,A,phi)) st x = <*g,(1_ A)*> holds
x " = <*(g "),(1_ A)*>
let x be Element of (semidirect_product (G,A,phi)); :: thesis: ( x = <*g,(1_ A)*> implies x " = <*(g "),(1_ A)*> )
assume A1: x = <*g,(1_ A)*> ; :: thesis: x " = <*(g "),(1_ A)*>
reconsider phi1 = phi . (1_ A), phi2 = phi . ((1_ A) ") as Homomorphism of G,G by AUTGROUP:def 1;
A2: phi . ((1_ A) ") = phi1 by GROUP_1:8;
thus x " = <*((phi . ((1_ A) ")) . (g ")),((1_ A) ")*> by A1, Th22
.= <*(phi1 . (g ")),(1_ A)*> by A2, GROUP_1:8
.= <*(g "),(1_ A)*> by Th15 ; :: thesis: verum