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 (Carrier F) 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 (Carrier F) 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 (Carrier F) 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 (Carrier F) 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 (Carrier F) ; :: 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 (Carrier F)) by A4, Th2;

then A5: rng f c= UF by A1, RELAT_1:def 19;

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 A2, A4, GROUP_19:9;

hence ( f0 in sum F & g = Product f0 ) by A4, GROUP_19:8, Th6; :: thesis: verum

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 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 (Carrier F) 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 (Carrier F) 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 (Carrier F) 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 (Carrier F) ; :: 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 (Carrier F)) by A4, Th2;

then A5: rng f c= UF by A1, RELAT_1:def 19;

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 A2, A4, GROUP_19:9;

hence ( f0 in sum F & g = Product f0 ) by A4, GROUP_19:8, Th6; :: thesis: verum