let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G) holds (Image (incl2 (G,A,phi))) /\ (Image (incl1 (G,A,phi))) = (1). (semidirect_product (G,A,phi))
let phi be Homomorphism of A,(AutGroup G); :: thesis: (Image (incl2 (G,A,phi))) /\ (Image (incl1 (G,A,phi))) = (1). (semidirect_product (G,A,phi))
set ImA = Image (incl2 (G,A,phi));
set ImG = Image (incl1 (G,A,phi));
set S = semidirect_product (G,A,phi);
for x being object st x in the carrier of ((Image (incl2 (G,A,phi))) /\ (Image (incl1 (G,A,phi)))) holds
x in {(1_ (semidirect_product (G,A,phi)))}

proof

let x be object ; :: thesis: ( x in the carrier of ((Image (incl2 (G,A,phi))) /\ (Image (incl1 (G,A,phi)))) implies x in {(1_ (semidirect_product (G,A,phi)))} )
assume x in the carrier of ((Image (incl2 (G,A,phi))) /\ (Image (incl1 (G,A,phi)))) ; :: thesis: x in {(1_ (semidirect_product (G,A,phi)))}
then x in (Image (incl2 (G,A,phi))) /\ (Image (incl1 (G,A,phi))) ;
then B1: ( x in Image (incl2 (G,A,phi)) & x in Image (incl1 (G,A,phi)) ) by GROUP_2:82;
then consider g being Element of G such that
B2: x = (incl1 (G,A,phi)) . g by GROUP_6:45;
consider a being Element of A such that
B3: x = (incl2 (G,A,phi)) . a by B1, GROUP_6:45;
<*(1_ G),a*> = x by B3, Def3
.= <*g,(1_ A)*> by B2, Def2 ;
then ( a = 1_ A & 1_ G = g ) by FINSEQ_1:77;
then x = <*(1_ G),(1_ A)*> by B2, Def2
.= 1_ (semidirect_product (G,A,phi)) by Th17 ;
hence x in {(1_ (semidirect_product (G,A,phi)))} by TARSKI:def 1; :: thesis: verum

end;

then the carrier of ((Image (incl2 (G,A,phi))) /\ (Image (incl1 (G,A,phi)))) c= {(1_ (semidirect_product (G,A,phi)))} ;
then the carrier of ((Image (incl2 (G,A,phi))) /\ (Image (incl1 (G,A,phi)))) c= the carrier of ((1). (semidirect_product (G,A,phi))) by GROUP_2:def 7;
then A1: (Image (incl2 (G,A,phi))) /\ (Image (incl1 (G,A,phi))) is Subgroup of (1). (semidirect_product (G,A,phi)) by GROUP_2:57;
(1). (semidirect_product (G,A,phi)) is Subgroup of (Image (incl2 (G,A,phi))) /\ (Image (incl1 (G,A,phi))) by GROUP_2:65;
hence (Image (incl2 (G,A,phi))) /\ (Image (incl1 (G,A,phi))) = (1). (semidirect_product (G,A,phi)) by A1, GROUP_2:55; :: thesis: verum