theorem
:: GROUP_19:18
for
I
being non
empty
set
for
F
being
Group-Family
of
I
for
x
being
Element
of
(
product
F
)
for
i
being
Element
of
I
for
g
being
Element
of
(
F
.
i
)
st
x
=
(
1_
(
product
F
)
)
+*
(
i
,
g
) &
g
<>
1_
(
F
.
i
)
holds
support
(
x
,
F
)
=
{
i
}