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 ;
a * b in a * B by ;
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 ;
then A6: (a * b) * ((b * a) ") in the carrier of B by ;
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 ;
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 ;
then (a * b) * ((b * a) ") in the carrier of A by ;
then (a * b) * ((b * a) ") in the carrier of A /\ the carrier of B by ;
then (a * b) * ((b * a) ") = 1_ G by ;
then (1_ G) * (b * a) = a * b by GROUP_1:14;
hence a * b = b * a by GROUP_1:def 4; :: thesis: verum