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