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_{1}[ 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_{1}[z,w]

A6: for z being Element of (product <*A,B*>) holds S_{1}[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

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)

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

( 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

( 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

proof

consider h being Function of (product <*A,B*>),G such that
let z be Element of (product <*A,B*>); :: thesis: ex w being Element of G st S_{1}[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_{1}[z,w]
by A4, A5; :: thesis: verum

end;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

A6: for z being Element of (product <*A,B*>) holds S

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 FINSEQ_1:44, A9 ;

b1 = <*a1,b1*> . 2 by FINSEQ_1:44

.= y by FINSEQ_1:44, A9 ;

hence h . <*a,b*> = a * b by A9, A10; :: thesis: verum

end;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 FINSEQ_1:44, A9 ;

b1 = <*a1,b1*> . 2 by FINSEQ_1:44

.= y by FINSEQ_1:44, A9 ;

hence h . <*a,b*> = a * b by A9, A10; :: thesis: verum

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

then A18:
h is one-to-one
by FUNCT_2:19;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;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

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

w in rng h

then
the carrier of G c= rng h
by TARSKI:def 3;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;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

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

then
h is Homomorphism of (product <*A,B*>),G
by GROUP_6:def 6;
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;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

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