let A be set ; for b being bag of A st Sum b = 0 holds
b = EmptyBag A
let b be bag of A; ( 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
; b = EmptyBag A
now not support b <> {} assume A4:
support b <> {}
;
contradictionconsider 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;
verum end;
hence
b = EmptyBag A
by PRE_POLY:81; verum