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

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