let G be Group; :: thesis: for H1, H2 being Subgroup of G st [.H1,H2.] = (1). G holds
for a, b being Element of G st a in H1 & b in H2 holds
a * b = b * a
let H1, H2 be Subgroup of G; :: thesis: ( [.H1,H2.] = (1). G implies for a, b being Element of G st a in H1 & b in H2 holds
a * b = b * a )
assume A1: [.H1,H2.] = (1). G ; :: thesis: for a, b being Element of G st a in H1 & b in H2 holds
a * b = b * a
let a, b be Element of G; :: thesis: ( a in H1 & b in H2 implies a * b = b * a )
assume A2: a in H1 ; :: thesis: ( not b in H2 or a * b = b * a )
assume A3: b in H2 ; :: thesis: a * b = b * a
[.a,b.] = 1_ G by A1, A2, A3, GROUP_5:1, GROUP_5:65;
hence a * b = b * a by GROUP_5:36; :: thesis: verum