let
L
be non
empty
ZeroStr
;
:: thesis:
for
a
being
Element
of
L
holds
(
a

L
)
.
0
=
a
let
a
be
Element
of
L
;
:: thesis:
(
a

L
)
.
0
=
a
0
in
NAT
;
then
0
in
dom
(
0_.
L
)
by
FUNCT_2:def 1
;
hence
a
=
(
a

L
)
.
0
by
FUNCT_7:31
;
:: thesis:
verum