let A be set ; :: thesis: for b being bag of st Sum b = 0 holds
b = EmptyBag A
let b be bag of ; :: thesis: ( Sum b = 0 implies b = EmptyBag A )
set cS = canFS (support b);
assume A1:
degree b = 0
; :: thesis: b = EmptyBag A
consider f being FinSequence of NAT such that
A2:
degree b = Sum f
and
A3:
f = b * (canFS (support b))
by Def4;
now assume A4:
support b <> {}
;
:: thesis: contradictionA5:
for
i being
Nat st
i in dom f holds
0 <= f . i
;
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:11;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 13;
support b c= dom b
by POLYNOM1:41;
then A9:
i in dom f
by A3, A6, A7, A8, FUNCT_1:21;
f . i = b . ((canFS (support b)) . i)
by A3, A7, FUNCT_1:23;
then
f . i <> 0
by A6, A8, POLYNOM1:def 7;
hence
ex
i being
Nat st
(
i in dom f &
0 < f . i )
by A9;
:: thesis: verum end; hence
contradiction
by A1, A2, A5, RVSUM_1:115;
:: thesis: verum end;
hence
b = EmptyBag A
by BAGORDER:20; :: thesis: verum