let I be set ; 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; 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); ( a in sum F iff support (a,F) is finite )
thus
( a in sum F implies support (a,F) is finite )
; ( support (a,F) is finite implies a in sum F )
assume
support (a,F) is finite
; 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 )
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
then
x = a
by A3, A10, Th3, FUNCT_1:2;
hence
a in sum F
; verum