for G being Group
for a being Element of G
for A being Subset of G holds
( a in gr A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) )