theorem
:: GROUP_19:22
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
support
(
x
,
F
) is
finite
holds
support
(
(
x
+*
(
i
,
g
)
)
,
F
) is
finite