set S = semidirect_product (G,A,phi);
reconsider e = <*(1_ G),(1_ A)*> as Element of (semidirect_product (G,A,phi)) by Th9;
take e ; :: according to GROUP_1:def 1 :: thesis: for b₁ being Element of the carrier of (semidirect_product (G,A,phi)) holds
( b₁ * e = b₁ & e * b₁ = b₁ )
let x be Element of (semidirect_product (G,A,phi)); :: thesis: ( x * e = x & e * x = x )
consider g being Element of G, a being Element of A such that
A1: x = <*g,a*> by Th12;
reconsider phi1 = phi . (1_ A), phia = phi . a as Homomorphism of G,G by AUTGROUP:def 1;
A2: (phi1 . g) * (1_ G) = g * (1_ G) by Th15
.= g by GROUP_1:def 4 ;
A3: phia . (1_ G) = 1_ G by GROUP_6:31;
thus x * e = <*(g * (phia . (1_ G))),(a * (1_ A))*> by A1, Th14
.= <*(g * (phia . (1_ G))),a*> by GROUP_1:def 4
.= x by A1, A3, GROUP_1:def 4 ; :: thesis: e * x = x
thus e * x = <*((1_ G) * (phi1 . g)),((1_ A) * a)*> by A1, Th14
.= <*((1_ G) * (phi1 . g)),a*> by GROUP_1:def 4
.= <*((1_ G) * g),a*> by A2, GROUP_1:def 4
.= x by A1, GROUP_1:def 4 ; :: thesis: verum