theorem
Th27
:
:: GROUP_19:27
for
I
being non
empty
set
for
F
being
Group-Family
of
I
for
i
being
Element
of
I
for
a
,
b
being
Function
st
dom
a
=
I
&
b
=
a
+*
(
i
,
(
1_
(
F
.
i
)
)
) holds
support
(
b
,
F
)
=
(
support
(
a
,
F
)
)
\
{
i
}