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 Def3;
assume A3: degree b = 0 ; :: thesis: b = EmptyBag A

now :: thesis: not support b <> {}

assume A4: support b <> {} ; :: thesis: contradiction
consider x being object such that
A5: x in support b by A4, XBOOLE_0:def 1;
x in rng (canFS (support b)) by A5, FUNCT_2:def 3;
then consider i being Nat such that
A6: i in dom (canFS (support b)) and
A7: (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, A6, FUNCT_1:13;
then A8: f . i <> 0 by A5, A7, PRE_POLY:def 7;
support b c= dom b by PRE_POLY:37;
then A9: ( i in dom f & 0 < f . i ) by A8, A2, A5, A6, A7, FUNCT_1:11;
for i being Nat st i in dom f holds
0 <= f . i ;
hence contradiction by A3, A1, A9, RVSUM_1:85; :: thesis: verum

end;

hence b = EmptyBag A by PRE_POLY:81; :: thesis: verum