let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G)
for x being Element of (semidirect_product (G,A,phi)) holds
( x . 1 in G & x . 2 in A & dom x = {1,2} )
let phi be Homomorphism of A,(AutGroup G); :: thesis: for x being Element of (semidirect_product (G,A,phi)) holds
( x . 1 in G & x . 2 in A & dom x = {1,2} )
let x be Element of (semidirect_product (G,A,phi)); :: thesis: ( x . 1 in G & x . 2 in A & dom x = {1,2} )
x in the carrier of (semidirect_product (G,A,phi)) ;
then x in the carrier of (product <*G,A*>) by Th9;
hence ( x . 1 in G & x . 2 in A & dom x = {1,2} ) by Th6; :: thesis: verum