let n be Ordinal; for b being bag of n holds
( TotDegree b = 0 iff b = EmptyBag n )
let b be bag of n; ( 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 ( b = EmptyBag n implies TotDegree b = 0 )
assume A4:
TotDegree b = 0
;
b = EmptyBag nconsider 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 for z being object st z in dom b holds
not b . z <> 0 let z be
object ;
( z in dom b implies not b . z <> 0 )assume that
z in dom b
and A8:
b . z <> 0
;
contradictionA9:
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;
verum end; then
b = n --> 0
by A3, FUNCOP_1:11;
hence
b = EmptyBag n
by PBOOLE:def 3;
verum
end;
assume
b = EmptyBag n
; 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;
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; verum