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