theorem
Th17
:
:: GROUP_19:17
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
) holds
support
(
x
,
F
)
c=
{
i
}