let n be Ordinal; for b being bag of n holds degree b = Sum (b * (SgmX ((RelIncl n),(support b))))
let b be bag of n; degree b = Sum (b * (SgmX ((RelIncl n),(support b))))
set SG = SgmX ((RelIncl n),(support b));
A1:
RelIncl n linearly_orders support b
by PRE_POLY:82;
A2:
rng (SgmX ((RelIncl n),(support b))) = support b
by A1, PRE_POLY:def 2;
then A3:
( rng (SgmX ((RelIncl n),(support b))) c= dom b & dom b = n )
by PRE_POLY:37, PARTFUN1:def 2;
consider f being FinSequence of NAT such that
A4:
( degree b = Sum f & f = b * (canFS (support b)) )
by UPROOTS:def 4;
rng (canFS (support b)) = support b
by FUNCT_2:def 3;
then reconsider C = canFS (support b) as FinSequence of n by FINSEQ_1:def 4;
rng b c= NAT
by VALUED_0:def 6;
then reconsider B = b as Function of n,REAL by A3, FUNCT_2:2;
A5:
SgmX ((RelIncl n),(support b)) is one-to-one
by PRE_POLY:10, PRE_POLY:82;
A6:
rng (SgmX ((RelIncl n),(support b))) = rng C
by FUNCT_2:def 3, A2;
then
for x being Element of n st x in (rng (SgmX ((RelIncl n),(support b)))) \ (rng C) holds
B . x = 0
by XBOOLE_0:def 1;
hence
degree b = Sum (b * (SgmX ((RelIncl n),(support b))))
by A4, ORDERS_5:8, A5, A6; verum