set
x
= the
Element
of
S
;
reconsider
x
= the
Element
of
S
as
Element
of
X
;
B
:
dom
(
Bag
S
)
=
X
by
PARTFUN1:def 2
;
(
Bag
S
)
.
x
=
1
by
UPROOTS:7
;
then
1
in
rng
(
Bag
S
)
by
B
,
FUNCT_1:3
;
then
rng
(
Bag
S
)
<>
{
0
}
by
TARSKI:def 1
;
hence
not
Bag
S
is
zero
by
bbbag
;
:: thesis:
verum