theorem
:: GROUP_19:29
for
I
being non
empty
set
for
F
being
GroupFamily
of
I
for
i
being
Element
of
I
for
a
being
Element
of
(
sum
F
)
for
b
being
Function
st
i
in
support
(
a
,
F
) &
b
=
a
+*
(
i
,
(
1_
(
F
.
i
)
)
) holds
card
(
support
(
b
,
F
)
)
=
(
card
(
support
(
a
,
F
)
)
)

1