theorem
Th25
:
:: GROUP_19:25
for
I
being non
empty
set
for
F
being
Group-Family
of
I
for
x
being
Function
for
i
being
Element
of
I
for
g
being
Element
of
(
F
.
i
)
st
x
in
sum
F
holds
x
+*
(
i
,
g
)
in
sum
F