let H, G be Group; :: thesis: for N being strict Group
for f being Homomorphism of N,G
for g being Homomorphism of H,G
for phi being Homomorphism of H,(AutGroup N) st ( for n being Element of N
for h being Element of H holds f . ((phi . h) . n) = ((g . h) * (f . n)) * (g . (h ")) ) holds
ex k being Homomorphism of (semidirect_product (N,H,phi)),G st
( f = k * (incl1 (N,H,phi)) & g = k * (incl2 (N,H,phi)) )
let N be strict Group; :: thesis: for f being Homomorphism of N,G
for g being Homomorphism of H,G
for phi being Homomorphism of H,(AutGroup N) st ( for n being Element of N
for h being Element of H holds f . ((phi . h) . n) = ((g . h) * (f . n)) * (g . (h ")) ) holds
ex k being Homomorphism of (semidirect_product (N,H,phi)),G st
( f = k * (incl1 (N,H,phi)) & g = k * (incl2 (N,H,phi)) )
let f be Homomorphism of N,G; :: thesis: for g being Homomorphism of H,G
for phi being Homomorphism of H,(AutGroup N) st ( for n being Element of N
for h being Element of H holds f . ((phi . h) . n) = ((g . h) * (f . n)) * (g . (h ")) ) holds
ex k being Homomorphism of (semidirect_product (N,H,phi)),G st
( f = k * (incl1 (N,H,phi)) & g = k * (incl2 (N,H,phi)) )
let g be Homomorphism of H,G; :: thesis: for phi being Homomorphism of H,(AutGroup N) st ( for n being Element of N
for h being Element of H holds f . ((phi . h) . n) = ((g . h) * (f . n)) * (g . (h ")) ) holds
ex k being Homomorphism of (semidirect_product (N,H,phi)),G st
( f = k * (incl1 (N,H,phi)) & g = k * (incl2 (N,H,phi)) )
let phi be Homomorphism of H,(AutGroup N); :: thesis: ( ( for n being Element of N
for h being Element of H holds f . ((phi . h) . n) = ((g . h) * (f . n)) * (g . (h ")) ) implies ex k being Homomorphism of (semidirect_product (N,H,phi)),G st
( f = k * (incl1 (N,H,phi)) & g = k * (incl2 (N,H,phi)) ) )
assume A1: for n being Element of N
for h being Element of H holds f . ((phi . h) . n) = ((g . h) * (f . n)) * (g . (h ")) ; :: thesis: ex k being Homomorphism of (semidirect_product (N,H,phi)),G st
( f = k * (incl1 (N,H,phi)) & g = k * (incl2 (N,H,phi)) )
set S = semidirect_product (N,H,phi);
defpred S₁[ Element of (semidirect_product (N,H,phi)), Element of G] means for n being Element of N
for h being Element of H st $1 = <*n,h*> holds
$2 = (f . n) * (g . h);
A2: for x being Element of (semidirect_product (N,H,phi)) ex y being Element of G st S₁[x,y]

proof

let x be Element of (semidirect_product (N,H,phi)); :: thesis: ex y being Element of G st S₁[x,y]
consider n being Element of N, h being Element of H such that
B1: x = <*n,h*> by Th12;
take y = (f . n) * (g . h); :: thesis: S₁[x,y]
for n1 being Element of N
for h1 being Element of H st x = <*n1,h1*> holds
y = (f . n1) * (g . h1)

proof

let n1 be Element of N; :: thesis: for h1 being Element of H st x = <*n1,h1*> holds
y = (f . n1) * (g . h1)
let h1 be Element of H; :: thesis: ( x = <*n1,h1*> implies y = (f . n1) * (g . h1) )
assume x = <*n1,h1*> ; :: thesis: y = (f . n1) * (g . h1)
then ( n = n1 & h = h1 ) by B1, FINSEQ_1:77;
hence y = (f . n1) * (g . h1) ; :: thesis: verum

end;

hence S₁[x,y] ; :: thesis: verum

end;

consider k being Function of (semidirect_product (N,H,phi)),G such that
A3: for x being Element of (semidirect_product (N,H,phi)) holds S₁[x,k . x] from FUNCT_2:sch 3(A2);
for x1, x2 being Element of (semidirect_product (N,H,phi)) holds k . (x1 * x2) = (k . x1) * (k . x2)

proof

let x1, x2 be Element of (semidirect_product (N,H,phi)); :: thesis: k . (x1 * x2) = (k . x1) * (k . x2)
consider n1 being Element of N, h1 being Element of H such that
B1: x1 = <*n1,h1*> by Th12;
consider n2 being Element of N, h2 being Element of H such that
B2: x2 = <*n2,h2*> by Th12;
reconsider phi1 = phi . h1 as Homomorphism of N,N by AUTGROUP:def 1;
x1 * x2 = <*(n1 * (phi1 . n2)),(h1 * h2)*> by B1, B2, Th14;
hence k . (x1 * x2) = (f . (n1 * (phi1 . n2))) * (g . (h1 * h2)) by A3
.= ((f . n1) * (f . (phi1 . n2))) * (g . (h1 * h2)) by GROUP_6:def 6
.= ((f . n1) * (((g . h1) * (f . n2)) * (g . (h1 ")))) * (g . (h1 * h2)) by A1
.= ((((f . n1) * (g . h1)) * (f . n2)) * (g . (h1 "))) * (g . (h1 * h2)) by LmAssoc
.= ((((f . n1) * (g . h1)) * (f . n2)) * (g . (h1 "))) * ((g . h1) * (g . h2)) by GROUP_6:def 6
.= (((((f . n1) * (g . h1)) * (f . n2)) * (g . (h1 "))) * (g . h1)) * (g . h2) by GROUP_1:def 3
.= ((((f . n1) * (g . h1)) * (f . n2)) * ((g . (h1 ")) * (g . h1))) * (g . h2) by GROUP_1:def 3
.= ((((f . n1) * (g . h1)) * (f . n2)) * (g . ((h1 ") * h1))) * (g . h2) by GROUP_6:def 6
.= ((((f . n1) * (g . h1)) * (f . n2)) * (g . (1_ H))) * (g . h2) by GROUP_1:def 5
.= ((((f . n1) * (g . h1)) * (f . n2)) * (1_ G)) * (g . h2) by GROUP_6:31
.= (((f . n1) * (g . h1)) * (f . n2)) * (g . h2) by GROUP_1:def 4
.= ((k . x1) * (f . n2)) * (g . h2) by A3, B1
.= (k . x1) * ((f . n2) * (g . h2)) by GROUP_1:def 3
.= (k . x1) * (k . x2) by A3, B2 ;
:: thesis: verum

end;

then reconsider k = k as Homomorphism of (semidirect_product (N,H,phi)),G by GROUP_6:def 6;
take k ; :: thesis: ( f = k * (incl1 (N,H,phi)) & g = k * (incl2 (N,H,phi)) )
A4: for n being Element of N
for h being Element of H holds k . <*n,h*> = (f . n) * (g . h)

proof

let n be Element of N; :: thesis: for h being Element of H holds k . <*n,h*> = (f . n) * (g . h)
let h be Element of H; :: thesis: k . <*n,h*> = (f . n) * (g . h)
reconsider x = <*n,h*> as Element of (semidirect_product (N,H,phi)) by Th9;
S₁[x,k . x] by A3;
hence k . <*n,h*> = (f . n) * (g . h) ; :: thesis: verum

end;

for n being Element of N holds f . n = (k * (incl1 (N,H,phi))) . n

proof

let n be Element of N; :: thesis: f . n = (k * (incl1 (N,H,phi))) . n
thus (k * (incl1 (N,H,phi))) . n = k . ((incl1 (N,H,phi)) . n) by FUNCT_2:15
.= k . <*n,(1_ H)*> by Def2
.= (f . n) * (g . (1_ H)) by A4
.= (f . n) * (1_ G) by GROUP_6:31
.= f . n by GROUP_1:def 4 ; :: thesis: verum

end;

hence f = k * (incl1 (N,H,phi)) by FUNCT_2:63; :: thesis: g = k * (incl2 (N,H,phi))
for h being Element of H holds g . h = (k * (incl2 (N,H,phi))) . h

proof

let h be Element of H; :: thesis: g . h = (k * (incl2 (N,H,phi))) . h
thus (k * (incl2 (N,H,phi))) . h = k . ((incl2 (N,H,phi)) . h) by FUNCT_2:15
.= k . <*(1_ N),h*> by Def3
.= (f . (1_ N)) * (g . h) by A4
.= (1_ G) * (g . h) by GROUP_6:31
.= g . h by GROUP_1:def 4 ; :: thesis: verum

end;

hence g = k * (incl2 (N,H,phi)) by FUNCT_2:63; :: thesis: verum