set x = the Element of X;
reconsider b = ({ the Element of X},1) -bag as bag of X ;
take b ; :: thesis: not b is zero
D: support b c= dom b by PRE_POLY:37;
the Element of X in { the Element of X} by TARSKI:def 1;
then A: b . the Element of X = 1 by UPROOTS:7;
then C: the Element of X in support b by PRE_POLY:def 7;
now :: thesis: not rng b = {0}
assume rng b = {0} ; :: thesis: contradiction
then b . the Element of X in {0} by C, D, FUNCT_1:3;
hence contradiction by A, TARSKI:def 1; :: thesis: verum
end;
hence not b is zero by bbbag; :: thesis: verum