let n be Ordinal; :: thesis: for b being bag of holds
( TotDegree b = 0 iff b = EmptyBag n )
let b be bag of ; :: thesis: ( TotDegree b = 0 iff b = EmptyBag n )
A1: field (RelIncl n) = n by WELLORD2:def 1;
RelIncl n is well-ordering by WELLORD2:7;
then RelIncl n is being_linear-order by ORDERS_1:107;
then A2: RelIncl n linearly_orders support b by A1, ORDERS_1:133, ORDERS_1:134;
A3: dom b = n by PARTFUN1:def 4;

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, Th5;

now

let z be set ; :: 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, TRIANG_1:def 2;
z in support b by A8, POLYNOM1:def 7;
then consider x being set 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 5;
x in dom f by A3, A6, A9, A10, RELAT_1:46;
then x in Seg (len f) by A7, FUNCOP_1:19;
then f . x = 0 by A7, FUNCOP_1:13;
hence contradiction by A6, A8, A10, A11, FUNCT_1:23; :: thesis: verum

end;

then b = n --> 0 by A3, FUNCOP_1:17;
hence b = EmptyBag n by POLYNOM1:def 15; :: thesis: verum

end;

assume b = EmptyBag n ; :: thesis: TotDegree b = 0
then A12: b = n --> 0 by POLYNOM1:def 15;
consider f being FinSequence of NAT such that
A13: TotDegree b = Sum f and
A14: f = b * (SgmX (RelIncl n),(support b)) by Def4;

now

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

end;

then rng (SgmX (RelIncl n),(support b)) = {} by A2, TRIANG_1:def 2;
then dom (SgmX (RelIncl n),(support b)) = {} by RELAT_1:65;
then dom (b * (SgmX (RelIncl n),(support b))) = {} by RELAT_1:44, XBOOLE_1:3;
hence TotDegree b = 0 by A13, A14, RELAT_1:64, RVSUM_1:102; :: thesis: verum