let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G)
for x being Element of (semidirect_product (G,A,phi)) ex g being Element of G ex a being Element of A st ((incl1 (G,A,phi)) . g) * ((incl2 (G,A,phi)) . a) = x
let phi be Homomorphism of A,(AutGroup G); :: thesis: for x being Element of (semidirect_product (G,A,phi)) ex g being Element of G ex a being Element of A st ((incl1 (G,A,phi)) . g) * ((incl2 (G,A,phi)) . a) = x
let x be Element of (semidirect_product (G,A,phi)); :: thesis: ex g being Element of G ex a being Element of A st ((incl1 (G,A,phi)) . g) * ((incl2 (G,A,phi)) . a) = x
consider g being Element of G, a being Element of A such that
A1: x = <*g,a*> by Th12;
take g ; :: thesis: ex a being Element of A st ((incl1 (G,A,phi)) . g) * ((incl2 (G,A,phi)) . a) = x
take a ; :: thesis: ((incl1 (G,A,phi)) . g) * ((incl2 (G,A,phi)) . a) = x
reconsider phi1 = phi . (1_ A) as Homomorphism of G,G by AUTGROUP:def 1;
( (incl1 (G,A,phi)) . g = <*g,(1_ A)*> & (incl2 (G,A,phi)) . a = <*(1_ G),a*> ) by Def2, Def3;
hence ((incl1 (G,A,phi)) . g) * ((incl2 (G,A,phi)) . a) = <*(g * (phi1 . (1_ G))),((1_ A) * a)*> by Th14
.= <*(g * (1_ G)),((1_ A) * a)*> by Th15
.= <*(g * (1_ G)),a*> by GROUP_1:def 4
.= x by A1, GROUP_1:def 4 ;
:: thesis: verum