let
V
be non
empty
addLoopStr
;
:: thesis:
for
v
being
Element
of
V
holds
(
ZeroLC
V
)
.
v
=
0
let
v
be
Element
of
V
;
:: thesis:
(
ZeroLC
V
)
.
v
=
0
(
Carrier
(
ZeroLC
V
)
=
{}
& not
v
in
{}
)
by
Def5
;
hence
(
ZeroLC
V
)
.
v
=
0
;
:: thesis:
verum