theorem Th11: :: GROUP_20:11

for I being non empty set
for G being Group
for F being component-commutative Subgroup-Family of I,G
for UF being Subset of G st UF = Union (Carrier F) holds
for g being Element of G
for H being FinSequence of G
for K being FinSequence of INT st len H = len K & rng H c= UF & Product (H |^ K) = g holds
ex f being finite-support Function of I,G st
( f in product F & g = Product f )