for x being set
for G being Group holds
( x in G ` 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 G & x = Product (F |^ I) ) )