theorem
Th41
:
:: MONOID_1:41
for
n
being
Element
of
NAT
for
A
being non
empty
set
for
a
being
Element
of
A
holds
(
|.
(
n
.-->
a
)
.|
.
a
=
n
& ( for
b
being
Element
of
A
st
b
<>
a
holds
|.
(
n
.-->
a
)
.|
.
b
=
0
) )