let n be Nat; :: thesis: for b being bag of n
for i being Nat st b . i = degree b holds
b = (EmptyBag n) +* (i,(b . i))
let b be bag of n; :: thesis: for i being Nat st b . i = degree b holds
b = (EmptyBag n) +* (i,(b . i))
let i be Nat; :: thesis: ( b . i = degree b implies b = (EmptyBag n) +* (i,(b . i)) )
assume A1: b . i = degree b ; :: thesis: b = (EmptyBag n) +* (i,(b . i))

per cases ( degree b = 0 or degree b > 0 ) ;

suppose degree b = 0 ; :: thesis: b = (EmptyBag n) +* (i,(b . i))

then A2: b = EmptyBag n by UPROOTS:12;
A3: ( dom ((EmptyBag n) +* (i,(b . i))) = n & n = dom b ) by PARTFUN1:def 2;
for x being object st x in dom b holds
b . x = ((EmptyBag n) +* (i,(b . i))) . x

proof

let x be object ; :: thesis: ( x in dom b implies b . x = ((EmptyBag n) +* (i,(b . i))) . x )
assume A4: x in dom b ; :: thesis: b . x = ((EmptyBag n) +* (i,(b . i))) . x

per cases ( x = i or x <> i ) ;

suppose x = i ; :: thesis: b . x = ((EmptyBag n) +* (i,(b . i))) . x

hence b . x = ((EmptyBag n) +* (i,(b . i))) . x by A4, A2, FUNCT_7:31; :: thesis: verum

end;

suppose x <> i ; :: thesis: b . x = ((EmptyBag n) +* (i,(b . i))) . x

hence b . x = ((EmptyBag n) +* (i,(b . i))) . x by A2, FUNCT_7:32; :: thesis: verum

end;

end;

end;

hence b = (EmptyBag n) +* (i,(b . i)) by A3; :: thesis: verum

end;

suppose A5: degree b > 0 ; :: thesis: b = (EmptyBag n) +* (i,(b . i))

then A6: ( i in dom b & dom b = n ) by A1, FUNCT_1:def 2, PARTFUN1:def 2;
set E = (EmptyBag n) +* (i,(b . i));
A7: dom (EmptyBag n) = n by PARTFUN1:def 2;
A8: b = (b +* (i,0)) + ((EmptyBag n) +* (i,(b . i))) by Th15;
then A9: Sum b = (Sum (b +* (i,0))) + (Sum ((EmptyBag n) +* (i,(b . i)))) by UPROOTS:15;
A10: support ((EmptyBag n) +* (i,(b . i))) = {i} by A5, A1, A6, Th13;
A11: RelIncl n linearly_orders support ((EmptyBag n) +* (i,(b . i))) by PRE_POLY:82;
set S = SgmX ((RelIncl n),(support ((EmptyBag n) +* (i,(b . i)))));
A12: ( rng (SgmX ((RelIncl n),(support ((EmptyBag n) +* (i,(b . i)))))) = {i} & len (SgmX ((RelIncl n),(support ((EmptyBag n) +* (i,(b . i)))))) = card {i} & card {i} = 1 ) by A10, A11, PRE_POLY:def 2, PRE_POLY:11, CARD_1:30;
{i} c= dom ((EmptyBag n) +* (i,(b . i))) by A10, PRE_POLY:37;
then A13: dom (((EmptyBag n) +* (i,(b . i))) * (SgmX ((RelIncl n),(support ((EmptyBag n) +* (i,(b . i))))))) = dom (SgmX ((RelIncl n),(support ((EmptyBag n) +* (i,(b . i)))))) by A12, RELAT_1:27;
then A14: len (((EmptyBag n) +* (i,(b . i))) * (SgmX ((RelIncl n),(support ((EmptyBag n) +* (i,(b . i))))))) = 1 by A12, FINSEQ_3:29;
1 in dom (((EmptyBag n) +* (i,(b . i))) * (SgmX ((RelIncl n),(support ((EmptyBag n) +* (i,(b . i))))))) by A13, FINSEQ_3:25, A12;
then ( (((EmptyBag n) +* (i,(b . i))) * (SgmX ((RelIncl n),(support ((EmptyBag n) +* (i,(b . i))))))) . 1 = ((EmptyBag n) +* (i,(b . i))) . ((SgmX ((RelIncl n),(support ((EmptyBag n) +* (i,(b . i)))))) . 1) & (SgmX ((RelIncl n),(support ((EmptyBag n) +* (i,(b . i)))))) . 1 in rng (SgmX ((RelIncl n),(support ((EmptyBag n) +* (i,(b . i)))))) ) by A13, FUNCT_1:12, FUNCT_1:def 3;
then (((EmptyBag n) +* (i,(b . i))) * (SgmX ((RelIncl n),(support ((EmptyBag n) +* (i,(b . i))))))) . 1 = ((EmptyBag n) +* (i,(b . i))) . i by A12, TARSKI:def 1;
then ((EmptyBag n) +* (i,(b . i))) * (SgmX ((RelIncl n),(support ((EmptyBag n) +* (i,(b . i)))))) = <*(((EmptyBag n) +* (i,(b . i))) . i)*> by A14, FINSEQ_1:40;
then Sum (((EmptyBag n) +* (i,(b . i))) * (SgmX ((RelIncl n),(support ((EmptyBag n) +* (i,(b . i))))))) = b . i by A7, A6, FUNCT_7:31;
then b . i = (Sum (b +* (i,0))) + (b . i) by A9, A1, HILB10_5:5;
then b +* (i,0) = EmptyBag n by UPROOTS:12;
hence b = (EmptyBag n) +* (i,(b . i)) by PRE_POLY:53, A8; :: thesis: verum

end;

end;