let
A
be non
empty
set
;
:: thesis:
for
a
being
Element
of
A
holds
|.
(
<*>
A
)
.|
.
a
=
0
let
a
be
Element
of
A
;
:: thesis:
|.
(
<*>
A
)
.|
.
a
=
0
dom
(
{
a
}
|`
{}
)
c=
dom
{}
by
FUNCT_1:56
;
then
dom
(
{
a
}
|`
(
<*>
A
)
)
=
{}
;
hence
|.
(
<*>
A
)
.|
.
a
=
0
by
Def7
,
CARD_1:27
;
:: thesis:
verum