let G be Group; :: thesis: for A, B being normal Subgroup of G st the carrier of A /\ the carrier of B = {(1_ G)} holds

for a, b being Element of G st a in A & b in B holds

a * b = b * a

let A, B be normal Subgroup of G; :: thesis: ( the carrier of A /\ the carrier of B = {(1_ G)} implies for a, b being Element of G st a in A & b in B holds

a * b = b * a )

assume A1: the carrier of A /\ the carrier of B = {(1_ G)} ; :: thesis: for a, b being Element of G st a in A & b in B holds

a * b = b * a

let a, b be Element of G; :: thesis: ( a in A & b in B implies a * b = b * a )

assume A2: ( a in A & b in B ) ; :: thesis: a * b = b * a

A3: (a * b) * ((b * a) ") = (a * b) * ((a ") * (b ")) by GROUP_1:17

.= ((a * b) * (a ")) * (b ") by GROUP_1:def 3 ;

A4: b " in B by A2, GROUP_2:51;

a * b in a * B by GROUP_2:27, A2;

then a * b in B * a by GROUP_3:117;

then consider s being Element of G such that

A5: ( a * b = s * a & s in the carrier of B ) by GROUP_2:28;

(a * b) * (a ") in B by GROUP_3:1, A5;

then A6: (a * b) * ((b * a) ") in the carrier of B by STRUCT_0:def 5, A3, A4, GROUP_2:50;

A7: (a * b) * ((b * a) ") = (a * b) * ((a ") * (b ")) by GROUP_1:17

.= a * (b * ((a ") * (b "))) by GROUP_1:def 3

.= a * ((b * (a ")) * (b ")) by GROUP_1:def 3 ;

a " in A by A2, GROUP_2:51;

then b * (a ") in b * A by GROUP_2:27;

then b * (a ") in A * b by GROUP_3:117;

then consider t being Element of G such that

A8: ( b * (a ") = t * b & t in the carrier of A ) by GROUP_2:28;

(b * (a ")) * (b ") in A by GROUP_3:1, A8;

then (a * b) * ((b * a) ") in the carrier of A by STRUCT_0:def 5, A7, A2, GROUP_2:50;

then (a * b) * ((b * a) ") in the carrier of A /\ the carrier of B by XBOOLE_0:def 4, A6;

then (a * b) * ((b * a) ") = 1_ G by A1, TARSKI:def 1;

then (1_ G) * (b * a) = a * b by GROUP_1:14;

hence a * b = b * a by GROUP_1:def 4; :: thesis: verum

for a, b being Element of G st a in A & b in B holds

a * b = b * a

let A, B be normal Subgroup of G; :: thesis: ( the carrier of A /\ the carrier of B = {(1_ G)} implies for a, b being Element of G st a in A & b in B holds

a * b = b * a )

assume A1: the carrier of A /\ the carrier of B = {(1_ G)} ; :: thesis: for a, b being Element of G st a in A & b in B holds

a * b = b * a

let a, b be Element of G; :: thesis: ( a in A & b in B implies a * b = b * a )

assume A2: ( a in A & b in B ) ; :: thesis: a * b = b * a

A3: (a * b) * ((b * a) ") = (a * b) * ((a ") * (b ")) by GROUP_1:17

.= ((a * b) * (a ")) * (b ") by GROUP_1:def 3 ;

A4: b " in B by A2, GROUP_2:51;

a * b in a * B by GROUP_2:27, A2;

then a * b in B * a by GROUP_3:117;

then consider s being Element of G such that

A5: ( a * b = s * a & s in the carrier of B ) by GROUP_2:28;

(a * b) * (a ") in B by GROUP_3:1, A5;

then A6: (a * b) * ((b * a) ") in the carrier of B by STRUCT_0:def 5, A3, A4, GROUP_2:50;

A7: (a * b) * ((b * a) ") = (a * b) * ((a ") * (b ")) by GROUP_1:17

.= a * (b * ((a ") * (b "))) by GROUP_1:def 3

.= a * ((b * (a ")) * (b ")) by GROUP_1:def 3 ;

a " in A by A2, GROUP_2:51;

then b * (a ") in b * A by GROUP_2:27;

then b * (a ") in A * b by GROUP_3:117;

then consider t being Element of G such that

A8: ( b * (a ") = t * b & t in the carrier of A ) by GROUP_2:28;

(b * (a ")) * (b ") in A by GROUP_3:1, A8;

then (a * b) * ((b * a) ") in the carrier of A by STRUCT_0:def 5, A7, A2, GROUP_2:50;

then (a * b) * ((b * a) ") in the carrier of A /\ the carrier of B by XBOOLE_0:def 4, A6;

then (a * b) * ((b * a) ") = 1_ G by A1, TARSKI:def 1;

then (1_ G) * (b * a) = a * b by GROUP_1:14;

hence a * b = b * a by GROUP_1:def 4; :: thesis: verum