let I be set ; :: thesis: for F being Group-Family of I
for a being Element of (sum F) ex J being finite Subset of I ex b being ManySortedSet of J st
( J = support (a,F) & a = (1_ (product F)) +* b & ( for j being object
for G being Group st j in I \ J & G = F . j holds
a . j = 1_ G ) & ( for j being object st j in J holds
a . j = b . j ) )
let F be Group-Family of I; :: thesis: for a being Element of (sum F) ex J being finite Subset of I ex b being ManySortedSet of J st
( J = support (a,F) & a = (1_ (product F)) +* b & ( for j being object
for G being Group st j in I \ J & G = F . j holds
a . j = 1_ G ) & ( for j being object st j in J holds
a . j = b . j ) )
let a be Element of (sum F); :: thesis: ex J being finite Subset of I ex b being ManySortedSet of J st
( J = support (a,F) & a = (1_ (product F)) +* b & ( for j being object
for G being Group st j in I \ J & G = F . j holds
a . j = 1_ G ) & ( for j being object st j in J holds
a . j = b . j ) )
consider g being Element of product (Carrier F), J being finite Subset of I, b being ManySortedSet of J such that
A1: ( g = 1_ (product F) & a = g +* b & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & b . j in the carrier of G & b . j <> 1_ G ) ) ) by GROUP_7:def 9;
take J ; :: thesis: ex b being ManySortedSet of J st
( J = support (a,F) & a = (1_ (product F)) +* b & ( for j being object
for G being Group st j in I \ J & G = F . j holds
a . j = 1_ G ) & ( for j being object st j in J holds
a . j = b . j ) )
take b ; :: thesis: ( J = support (a,F) & a = (1_ (product F)) +* b & ( for j being object
for G being Group st j in I \ J & G = F . j holds
a . j = 1_ G ) & ( for j being object st j in J holds
a . j = b . j ) )
A2: dom b = J by PARTFUN1:def 2;
A3: dom (1_ (product F)) = I by Th3;
A4: for j being object
for G being Group st j in I \ J & G = F . j holds
a . j = 1_ G

proof

let j be object ; :: thesis: for G being Group st j in I \ J & G = F . j holds
a . j = 1_ G
let G be Group; :: thesis: ( j in I \ J & G = F . j implies a . j = 1_ G )
assume that
A6: j in I \ J and
A7: G = F . j ; :: thesis: a . j = 1_ G
( j in dom (1_ (product F)) & not j in dom b ) by A3, A6, XBOOLE_0:def 5;
hence a . j = (1_ (product F)) . j by A1, FUNCT_4:11
.= 1_ G by A6, A7, GROUP_7:6 ;
:: thesis: verum

end;

for j being object holds
( j in support (a,F) iff j in J )

proof

let j be object ; :: thesis: ( j in support (a,F) iff j in J )

hereby :: thesis: ( j in J implies j in support (a,F) )

assume A11: j in support (a,F) ; :: thesis: j in J
then consider G being Group such that
A12: ( G = F . j & a . j <> 1_ G & j in I ) by Def1;
assume not j in J ; :: thesis: contradiction
then j in I \ J by A11, XBOOLE_0:def 5;
hence contradiction by A4, A12; :: thesis: verum

end;

assume A13: j in J ; :: thesis: j in support (a,F)
then consider G being non empty Group-like multMagma such that
A14: ( G = F . j & b . j in the carrier of G & b . j <> 1_ G ) by A1;
a . j <> 1_ G by A1, A2, A13, A14, FUNCT_4:13;
hence j in support (a,F) by A13, A14, Def1; :: thesis: verum

end;

hence ( J = support (a,F) & a = (1_ (product F)) +* b & ( for j being object
for G being Group st j in I \ J & G = F . j holds
a . j = 1_ G ) & ( for j being object st j in J holds
a . j = b . j ) ) by A1, A2, A4, FUNCT_4:13, TARSKI:2; :: thesis: verum