theorem
Th31
:
:: MONOID_1:31
for
A
being non
empty
set
for
a
,
b
being
Element
of
A
holds
(
(
chi
a
)
.
a
=
1 & (
b
<>
a
implies
(
chi
a
)
.
b
=
0
) )