let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G) holds 1_ (semidirect_product (G,A,phi)) = <*(1_ G),(1_ A)*>
let phi be Homomorphism of A,(AutGroup G); :: thesis: 1_ (semidirect_product (G,A,phi)) = <*(1_ G),(1_ A)*>
reconsider e = <*(1_ G),(1_ A)*> as Element of (semidirect_product (G,A,phi)) by Th9;
for x being Element of (semidirect_product (G,A,phi)) holds
( x * e = x & e * x = x ) by Lm4;
hence 1_ (semidirect_product (G,A,phi)) = <*(1_ G),(1_ A)*> by GROUP_1:def 4; :: thesis: verum