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;

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}

hence
not b is zero
by bbbag; :: thesis: verumassume
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;then b . the Element of X in {0} by C, D, FUNCT_1:3;

hence contradiction by A, TARSKI:def 1; :: thesis: verum