let n be Ordinal; :: thesis: for b being bag of n holds degree b = Sum (b * (SgmX ((RelIncl n),(support b))))
let b be bag of n; :: thesis: 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; :: thesis: verum