let G be Group; :: thesis: for A, B being normal Subgroup of G st ( for x being Element of G ex a, b being Element of G st
( a in A & b in B & x = a * b ) ) & the carrier of A /\ the carrier of B = {(1_ G)} holds
ex h being Homomorphism of (product <*A,B*>),G st
( h is bijective & ( for a, b being Element of G st a in A & b in B holds
h . <*a,b*> = a * b ) )
let A, B be normal Subgroup of G; :: thesis: ( ( for x being Element of G ex a, b being Element of G st
( a in A & b in B & x = a * b ) ) & the carrier of A /\ the carrier of B = {(1_ G)} implies ex h being Homomorphism of (product <*A,B*>),G st
( h is bijective & ( for a, b being Element of G st a in A & b in B holds
h . <*a,b*> = a * b ) ) )
assume A1: for x being Element of G ex a, b being Element of G st
( a in A & b in B & x = a * b ) ; :: thesis: ( not the carrier of A /\ the carrier of B = {(1_ G)} or ex h being Homomorphism of (product <*A,B*>),G st
( h is bijective & ( for a, b being Element of G st a in A & b in B holds
h . <*a,b*> = a * b ) ) )
assume A2: the carrier of A /\ the carrier of B = {(1_ G)} ; :: thesis: ex h being Homomorphism of (product <*A,B*>),G st
( h is bijective & ( for a, b being Element of G st a in A & b in B holds
h . <*a,b*> = a * b ) )
defpred S₁[ set , set ] means ex x, y being Element of G st
( x in A & y in B & $1 = <*x,y*> & $2 = x * y );
A3: for z being Element of (product <*A,B*>) ex w being Element of G st S₁[z,w]

proof

let z be Element of (product <*A,B*>); :: thesis: ex w being Element of G st S₁[z,w]
consider x being Element of A, y being Element of B such that
A4: z = <*x,y*> by TOPALG_4:1;
reconsider x1 = x, y1 = y as Element of G by GROUP_2:41, STRUCT_0:def 5;
A5: x1 * y1 is Element of G ;
( x1 in A & y1 in B ) ;
hence ex w being Element of G st S₁[z,w] by A4, A5; :: thesis: verum

end;

consider h being Function of (product <*A,B*>),G such that
A6: for z being Element of (product <*A,B*>) holds S₁[z,h . z] from FUNCT_2:sch 3(A3);
A7: for a, b being Element of G st a in A & b in B holds
h . <*a,b*> = a * b

proof

let a, b be Element of G; :: thesis: ( a in A & b in B implies h . <*a,b*> = a * b )
assume A8: ( a in A & b in B ) ; :: thesis: h . <*a,b*> = a * b
then reconsider a1 = a as Element of A ;
reconsider b1 = b as Element of B by A8;
consider x, y being Element of G such that
A9: ( x in A & y in B & <*a1,b1*> = <*x,y*> & h . <*a1,b1*> = x * y ) by A6;
A10: a1 = <*a1,b1*> . 1
.= x by FINSEQ_1:44, A9 ;
b1 = <*a1,b1*> . 2
.= y by FINSEQ_1:44, A9 ;
hence h . <*a,b*> = a * b by A9, A10; :: thesis: verum

end;

now :: thesis: for z1, z2 being object st z1 in the carrier of (product <*A,B*>) & z2 in the carrier of (product <*A,B*>) & h . z1 = h . z2 holds
z1 = z2

let z1, z2 be object ; :: thesis: ( z1 in the carrier of (product <*A,B*>) & z2 in the carrier of (product <*A,B*>) & h . z1 = h . z2 implies z1 = z2 )
assume A11: ( z1 in the carrier of (product <*A,B*>) & z2 in the carrier of (product <*A,B*>) & h . z1 = h . z2 ) ; :: thesis: z1 = z2
then consider x1, y1 being Element of G such that
A12: ( x1 in A & y1 in B & z1 = <*x1,y1*> & h . z1 = x1 * y1 ) by A6;
consider x2, y2 being Element of G such that
A13: ( x2 in A & y2 in B & z2 = <*x2,y2*> & h . z2 = x2 * y2 ) by A6, A11;
x1 = (x2 * y2) * (y1 ") by GROUP_1:14, A13, A11, A12;
then x1 = x2 * (y2 * (y1 ")) by GROUP_1:def 3;
then A14: (x2 ") * x1 = y2 * (y1 ") by GROUP_1:13;
x2 " in A by A13, GROUP_2:51;
then A15: (x2 ") * x1 in the carrier of A by GROUP_2:50, A12, STRUCT_0:def 5;
y1 " in B by A12, GROUP_2:51;
then y2 * (y1 ") in the carrier of B by A13, GROUP_2:50, STRUCT_0:def 5;
then A16: (x2 ") * x1 in the carrier of A /\ the carrier of B by A14, A15, XBOOLE_0:def 4;
then (x2 ") * x1 = 1_ G by A2, TARSKI:def 1;
then x1 = x2 * (1_ G) by GROUP_1:13;
then A17: x1 = x2 by GROUP_1:def 4;
y2 * (y1 ") = 1_ G by A2, TARSKI:def 1, A14, A16;
then y2 = (1_ G) * y1 by GROUP_1:14;
hence z1 = z2 by A12, A13, A17, GROUP_1:def 4; :: thesis: verum

end;

then A18: h is one-to-one by FUNCT_2:19;

now :: thesis: for w being object st w in the carrier of G holds
w in rng h

let w be object ; :: thesis: ( w in the carrier of G implies w in rng h )
assume w in the carrier of G ; :: thesis: w in rng h
then reconsider g = w as Element of G ;
consider a, b being Element of G such that
A19: ( a in A & b in B & g = a * b ) by A1;
reconsider a1 = a as Element of A by A19;
reconsider b1 = b as Element of B by A19;
h . <*a1,b1*> = a * b by A7, A19;
hence w in rng h by A19, FUNCT_2:112; :: thesis: verum

end;

then the carrier of G c= rng h by TARSKI:def 3;
then A20: h is onto by FUNCT_2:def 3, XBOOLE_0:def 10;
for z, w being Element of (product <*A,B*>) holds h . (z * w) = (h . z) * (h . w)

proof

let z, w be Element of (product <*A,B*>); :: thesis: h . (z * w) = (h . z) * (h . w)
consider x being Element of A, y being Element of B such that
A21: z = <*x,y*> by TOPALG_4:1;
reconsider x1 = x, y1 = y as Element of G by GROUP_2:41, STRUCT_0:def 5;
consider a being Element of A, b being Element of B such that
A22: w = <*a,b*> by TOPALG_4:1;
reconsider a1 = a, b1 = b as Element of G by GROUP_2:41, STRUCT_0:def 5;
A23: y * b = y1 * b1 by GROUP_2:43;
A24: z * w = <*(x * a),(y * b)*> by A21, A22, GROUP_7:29
.= <*(x1 * a1),(y1 * b1)*> by GROUP_2:43, A23 ;
A25: ( x1 in A & a1 in A ) ;
then A26: x1 * a1 in A by GROUP_2:50;
A27: ( y1 in B & b1 in B ) ;
then A28: y1 * b1 in B by GROUP_2:50;
A29: h . (z * w) = (x1 * a1) * (y1 * b1) by A7, A24, A26, A28
.= x1 * (a1 * (y1 * b1)) by GROUP_1:def 3
.= x1 * ((a1 * y1) * b1) by GROUP_1:def 3
.= x1 * ((y1 * a1) * b1) by Th11, A2, A25, A27
.= x1 * (y1 * (a1 * b1)) by GROUP_1:def 3
.= (x1 * y1) * (a1 * b1) by GROUP_1:def 3 ;
h . z = x1 * y1 by A21, A7, A25, A27;
hence h . (z * w) = (h . z) * (h . w) by A29, A22, A7, A25, A27; :: thesis: verum

end;

then h is Homomorphism of (product <*A,B*>),G by GROUP_6:def 6;
hence ex h being Homomorphism of (product <*A,B*>),G st
( h is bijective & ( for a, b being Element of G st a in A & b in B holds
h . <*a,b*> = a * b ) ) by A7, A20, A18; :: thesis: verum