theorem :: GROUP_23:71

for G being Group
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