let I be non empty set ; :: thesis: for G being Group
for F being component-commutative Subgroup-Family of I,G
for UF being Subset of G st UF = Union () holds
for g being Element of G st g in gr UF holds
ex f being finite-support Function of I,(gr UF) st
( f in sum F & g = Product f )

let G be Group; :: thesis: for F being component-commutative Subgroup-Family of I,G
for UF being Subset of G st UF = Union () holds
for g being Element of G st g in gr UF holds
ex f being finite-support Function of I,(gr UF) st
( f in sum F & g = Product f )

let F be component-commutative Subgroup-Family of I,G; :: thesis: for UF being Subset of G st UF = Union () holds
for g being Element of G st g in gr UF holds
ex f being finite-support Function of I,(gr UF) st
( f in sum F & g = Product f )

let UF be Subset of G; :: thesis: ( UF = Union () implies for g being Element of G st g in gr UF holds
ex f being finite-support Function of I,(gr UF) st
( f in sum F & g = Product f ) )

assume A1: UF = Union () ; :: thesis: for g being Element of G st g in gr UF holds
ex f being finite-support Function of I,(gr UF) st
( f in sum F & g = Product f )

A2: for i being object st i in I holds
F . i is Subgroup of G by Def1;
let g be Element of G; :: thesis: ( g in gr UF implies ex f being finite-support Function of I,(gr UF) st
( f in sum F & g = Product f ) )

assume g in gr UF ; :: thesis: ex f being finite-support Function of I,(gr UF) st
( f in sum F & g = Product f )

then consider H being FinSequence of G, K being FinSequence of INT such that
A3: ( len H = len K & rng H c= UF & Product (H |^ K) = g ) by GROUP_4:28;
consider f being finite-support Function of I,G such that
A4: ( f in product F & g = Product f ) by A1, A3, Th11;
f is Function of I,(Union ()) by ;
then A5: rng f c= UF by ;
UF c= [#] (gr UF) by GROUP_4:def 4;
then rng f c= [#] (gr UF) by A5;
then reconsider f0 = f as finite-support Function of I,(gr UF) by Th5;
take f0 ; :: thesis: ( f0 in sum F & g = Product f0 )
support (f,F) = support f by ;
hence ( f0 in sum F & g = Product f0 ) by ; :: thesis: verum