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