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