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 S1[ 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 S1[z,w]
proof
let z be Element of (product <*A,B*>); :: thesis: ex w being Element of G st S1[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 ;
A5: x1 * y1 is Element of G ;
( x1 in A & y1 in B ) ;
hence ex w being Element of G st S1[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 S1[z,h . z] from 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 by FINSEQ_1:44
.= x by ;
b1 = <*a1,b1*> . 2 by FINSEQ_1:44
.= y by ;
hence h . <*a,b*> = a * b by ; :: 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 ;
x1 = (x2 * y2) * (y1 ") by ;
then x1 = x2 * (y2 * (y1 ")) by GROUP_1:def 3;
then A14: (x2 ") * x1 = y2 * (y1 ") by GROUP_1:13;
x2 " in A by ;
then A15: (x2 ") * x1 in the carrier of A by ;
y1 " in B by ;
then y2 * (y1 ") in the carrier of B by ;
then A16: (x2 ") * x1 in the carrier of A /\ the carrier of B by ;
then (x2 ") * x1 = 1_ G by ;
then x1 = x2 * (1_ G) by GROUP_1:13;
then A17: x1 = x2 by GROUP_1:def 4;
y2 * (y1 ") = 1_ G by ;
then y2 = (1_ G) * y1 by GROUP_1:14;
hence z1 = z2 by ; :: 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 ;
hence w in rng h by ; :: thesis: verum
end;
then the carrier of G c= rng h by TARSKI:def 3;
then A20: h is onto by ;
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 ;
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 ;
A23: y * b = y1 * b1 by GROUP_2:43;
A24: z * w = <*(x * a),(y * b)*> by
.= <*(x1 * a1),(y1 * b1)*> by ;
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