theorem
Th51
:
:: GROUP_19:51
for
I
being non
empty
set
for
G
being
Group
for
a
being
finitesupport
Function
of
I
,
G
for
W
being
finite
Subset
of
I
st
support
a
c=
W
& ( for
i
,
j
being
Element
of
I
holds
(
a
.
i
)
*
(
a
.
j
)
=
(
a
.
j
)
*
(
a
.
i
)
) holds
Product
a
=
Product
(
a

W
)