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;

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;

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

( 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
b = EmptyBag n
; :: thesis: 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;

hence b = EmptyBag n by PBOOLE:def 3; :: thesis: verum

end;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

then
b = n --> 0
by A3, FUNCOP_1:11;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;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

hence b = EmptyBag n by PBOOLE:def 3; :: thesis: verum

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

then
rng (SgmX ((RelIncl n),(support b))) = {}
by A2, PRE_POLY:def 2;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 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

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