let I be set ; :: thesis: for F being Group-Family of I
for a being Element of (product F) holds
( a in sum F iff support (a,F) is finite )
let F be Group-Family of I; :: thesis: for a being Element of (product F) holds
( a in sum F iff support (a,F) is finite )
let a be Element of (product F); :: thesis: ( a in sum F iff support (a,F) is finite )
thus ( a in sum F implies support (a,F) is finite ) ; :: thesis: ( support (a,F) is finite implies a in sum F )
assume support (a,F) is finite ; :: thesis: a in sum F
then reconsider J = support (a,F) as finite Subset of I ;
A2: [#] (product F) = product (Carrier F) by GROUP_7:def 2;
set k = a | J;
A3: dom a = I by A2, PARTFUN1:def 2;
then A4: dom (a | J) = J by RELAT_1:62;
then reconsider k = a | J as ManySortedSet of J by PARTFUN1:def 2, RELAT_1:def 18;
set x = (1_ (product F)) +* k;
A5: 1_ (product F) is Element of product (Carrier F) by GROUP_7:def 2;
for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & k . j in the carrier of G & k . j <> 1_ G )

proof

let j be set ; :: thesis: ( j in J implies ex G being non empty Group-like multMagma st
( G = F . j & k . j in the carrier of G & k . j <> 1_ G ) )
assume A6: j in J ; :: thesis: ex G being non empty Group-like multMagma st
( G = F . j & k . j in the carrier of G & k . j <> 1_ G )
then consider G being Group such that
A: ( G = F . j & a . j <> 1_ G & j in I ) by Def1;
take G ; :: thesis: ( G = F . j & k . j in the carrier of G & k . j <> 1_ G )
thus G = F . j by A; :: thesis: ( k . j in the carrier of G & k . j <> 1_ G )
a in product F ;
then a . j in G by A, Th5;
hence k . j in the carrier of G by A6, FUNCT_1:49; :: thesis: k . j <> 1_ G
thus k . j <> 1_ G by A, A6, FUNCT_1:49; :: thesis: verum

end;

then reconsider x = (1_ (product F)) +* k as Element of (sum F) by A5, GROUP_7:def 9;
x in sum F ;
then A10: x in product F by GROUP_2:40;
then A11: dom x = I by Th3;
for i being object st i in dom x holds
x . i = a . i

proof

let i be object ; :: thesis: ( i in dom x implies x . i = a . i )
assume A12: i in dom x ; :: thesis: x . i = a . i
then reconsider G = F . i as Group by A11, Th1;

per cases ( not i in J or i in J ) ;

suppose A15: not i in J ; :: thesis: x . i = a . i

then not i in dom k ;
then x . i = (1_ (product F)) . i by FUNCT_4:11
.= 1_ G by A11, A12, GROUP_7:6 ;
hence x . i = a . i by A11, A12, A15, Def1; :: thesis: verum

end;

suppose A16: i in J ; :: thesis: x . i = a . i

hence x . i = k . i by A4, FUNCT_4:13
.= a . i by A16, FUNCT_1:49 ;
:: thesis: verum

end;

end;

end;

then x = a by A3, A10, Th3, FUNCT_1:2;
hence a in sum F ; :: thesis: verum