let A be set ; :: thesis: for b being bag of A st Sum b = 0 holds
b = EmptyBag A
let b be bag of A; :: thesis: ( Sum b = 0 implies b = EmptyBag A )
set cS = canFS (support b);
consider f being FinSequence of NAT such that
A1: degree b = Sum f and
A2: f = b * (canFS (support b)) by Def4;
assume A3: degree b = 0 ; :: thesis: b = EmptyBag A

now

assume A4: support b <> {} ; :: thesis: contradiction

A5: now

consider x being set such that
A6: x in support b by A4, XBOOLE_0:def 1;
x in rng (canFS (support b)) by A6, FUNCT_2:def 3;
then consider i being Nat such that
A7: i in dom (canFS (support b)) and
A8: (canFS (support b)) . i = x by FINSEQ_2:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
f . i = b . ((canFS (support b)) . i) by A2, A7, FUNCT_1:13;
then A9: f . i <> 0 by A6, A8, PRE_POLY:def 7;
support b c= dom b by PRE_POLY:37;
then i in dom f by A2, A6, A7, A8, FUNCT_1:11;
hence ex i being Nat st
( i in dom f & 0 < f . i ) by A9; :: thesis: verum

end;

for i being Nat st i in dom f holds
0 <= f . i ;
hence contradiction by A3, A1, A5, RVSUM_1:85; :: thesis: verum

end;

hence b = EmptyBag A by BAGORDER:19; :: thesis: verum