theorem :: GROUP_5:64

for x being set
for G being Group
for H1, H2 being Subgroup of G holds
( x in [.H1,H2.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators (H1,H2) & x = Product (F |^ I) ) ) by Th61;