let n be Ordinal; :: thesis: for b being bag of n holds
( TotDegree b = 0 iff b = EmptyBag n )
let b be bag of n; :: thesis: ( TotDegree b = 0 iff b = EmptyBag n )
A1: field (RelIncl n) = n by WELLORD2:def 1;
RelIncl n is being_linear-order by ORDERS_1:19;
then A2: RelIncl n linearly_orders support b by A1, ORDERS_1:37, ORDERS_1:38;
A3: dom b = n by PARTFUN1:def 2;

hereby :: thesis: ( b = EmptyBag n implies TotDegree b = 0 )

assume A4: TotDegree b = 0 ; :: thesis: b = EmptyBag n
consider f being FinSequence of NAT such that
A5: TotDegree b = Sum f and
A6: f = b * (SgmX ((RelIncl n),(support b))) by Def4;
A7: f = (len f) |-> 0 by A4, A5, Th3;

now :: thesis: for z being object st z in dom b holds
not b . z <> 0

let z be object ; :: thesis: ( z in dom b implies not b . z <> 0 )
assume that
z in dom b and
A8: b . z <> 0 ; :: thesis: contradiction
A9: rng (SgmX ((RelIncl n),(support b))) = support b by A2, PRE_POLY:def 2;
z in support b by A8, PRE_POLY:def 7;
then consider x being object such that
A10: x in dom (SgmX ((RelIncl n),(support b))) and
A11: (SgmX ((RelIncl n),(support b))) . x = z by A9, FUNCT_1:def 3;
x in dom f by A3, A6, A9, A10, RELAT_1:27;
then x in Seg (len f) by A7, FUNCOP_1:13;
then f . x = 0 by A7, FUNCOP_1:7;
hence contradiction by A6, A8, A10, A11, FUNCT_1:13; :: thesis: verum

end;

then b = n --> 0 by A3, FUNCOP_1:11;
hence b = EmptyBag n by PBOOLE:def 3; :: thesis: verum

end;

assume b = EmptyBag n ; :: thesis: TotDegree b = 0
then A12: b = n --> 0 by PBOOLE:def 3;
A13: ex f being FinSequence of NAT st
( TotDegree b = Sum f & f = b * (SgmX ((RelIncl n),(support b))) ) by Def4;

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

assume support b <> {} ; :: thesis: contradiction
then consider x being object such that
A14: x in support b by XBOOLE_0:def 1;
b . x = 0 by A12, A14, FUNCOP_1:7;
hence contradiction by A14, PRE_POLY:def 7; :: thesis: verum

end;

then rng (SgmX ((RelIncl n),(support b))) = {} by A2, PRE_POLY:def 2;
then dom (SgmX ((RelIncl n),(support b))) = {} by RELAT_1:42;
then dom (b * (SgmX ((RelIncl n),(support b)))) = {} by RELAT_1:25, XBOOLE_1:3;
hence TotDegree b = 0 by A13, RELAT_1:41, RVSUM_1:72; :: thesis: verum