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 x = <*g,a*>
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 x = <*g,a*>
let x be Element of (semidirect_product (G,A,phi)); :: thesis: ex g being Element of G ex a being Element of A st x = <*g,a*>
( x . 1 in G & x . 2 in A ) by Th11;
then consider g being Element of G, a being Element of A such that
A1: ( g = x . 1 & a = x . 2 ) ;
take g ; :: thesis: ex a being Element of A st x = <*g,a*>
take a ; :: thesis: x = <*g,a*>
dom x = {1,2} by Th11;
then len x = 2 by FINSEQ_1:2, FINSEQ_1:def 3;
hence x = <*g,a*> by A1, FINSEQ_1:44; :: thesis: verum