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

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 <> {}

hence
b = EmptyBag A
by PRE_POLY:81; :: thesis: verumassume 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;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