let n be Ordinal; :: thesis:
let a, b be bag of ; :: thesis:
A1: field (RelIncl n) = n by WELLORD2:def 1;
RelIncl n is well-ordering by WELLORD2:7;
then A2: RelIncl n is being_linear-order by ORDERS_1:107;
consider fab being FinSequence of NAT such that
A3: TotDegree (a + b) = Sum fab and
A4: fab = (a + b) * (SgmX (RelIncl n),(support (a + b))) by Def4;
consider fa being FinSequence of NAT such that
A5: TotDegree a = Sum fa and
A6: fa = a * (SgmX (RelIncl n),(support a)) by Def4;
consider fb being FinSequence of NAT such that
A7: TotDegree b = Sum fb and
A8: fb = b * (SgmX (RelIncl n),(support b)) by Def4;
reconsider fab' = fab as FinSequence of REAL by FINSEQ_2:27;
set sasb = (support a) \/ (support b);
reconsider sasb = (support a) \/ (support b) as finite Subset of n ;
set s = SgmX (RelIncl n),sasb;
set fa'b = a * (SgmX (RelIncl n),sasb);
set fb'a = b * (SgmX (RelIncl n),sasb);
RelIncl n linearly_orders sasb by A1, A2, ORDERS_1:133, ORDERS_1:134;
then A9: rng (SgmX (RelIncl n),sasb) = sasb by TRIANG_1:def 2;
A10: support (a + b) = sasb by POLYNOM1:42;
A11: ( dom a = n & dom b = n ) by PARTFUN1:def 4;
then reconsider fa'b = a * (SgmX (RelIncl n),sasb), fb'a = b * (SgmX (RelIncl n),sasb) as FinSequence by A9, FINSEQ_1:20;
A12: ( rng fa'b c= rng a & rng fb'a c= rng b ) by RELAT_1:45;
A13: ( rng fa'b c= NAT & rng fb'a c= NAT ) by VALUED_0:def 6;
( rng fa'b c= REAL & rng fb'a c= REAL ) by A12, XBOOLE_1:1;
then reconsider fa'b = fa'b, fb'a = fb'a as FinSequence of REAL by FINSEQ_1:def 4;
reconsider fa'bn = fa'b, fb'an = fb'a as FinSequence of NAT by A13, FINSEQ_1:def 4;
set ln = len fab;
A14: dom (a + b) = n by PARTFUN1:def 4;
A15: Seg (len fab) = dom fab by FINSEQ_1:def 3
.= dom (SgmX (RelIncl n),sasb) by A4, A9, A10, A14, RELAT_1:46 ;
then A16: Seg (len fab) = dom fa'b by A9, A11, RELAT_1:46;
A17: Seg (len fab) = dom fb'a by A9, A11, A15, RELAT_1:46;
A18: Sum fa = Sum fa'bn by A6, Th13;
A19: Sum fb = Sum fb'an by A8, Th13;
A20: len fa'b = len fb'a by A16, A17, FINSEQ_3:31;
then A21: len (fa'b + fb'a) = len fa'b by INTEGRA5:2;
then A22: Seg (len fab) = dom (fa'b + fb'a) by A16, FINSEQ_3:31;
reconsider fa'b' = fa'b as natural-valued ManySortedSet of by A16, PARTFUN1:def 4, RELAT_1:def 18;

now

thus Seg (len fab) = dom fab' by FINSEQ_1:def 3; :: thesis:
thus Seg (len fab) = dom (fa'b + fb'a) by A16, A21, FINSEQ_3:31; :: thesis:
let k be Nat; :: thesis:
assume A23: k in Seg (len fab) ; :: thesis:
reconsider k1 = k as Element of NAT by ORDINAL1:def 13;
reconsider fa'bk = fa'b . k1, fb'ak = fb'a . k1 as Real ;
thus fab' . k = (a + b) . ((SgmX (RelIncl n),(support (a + b))) . k) by A4, A10, A15, A23, FUNCT_1:23
.= (a . ((SgmX (RelIncl n),(support (a + b))) . k)) + (b . ((SgmX (RelIncl n),(support (a + b))) . k)) by POLYNOM1:def 5
.= (fa'b' . k) + (b . ((SgmX (RelIncl n),(support (a + b))) . k)) by A10, A15, A23, FUNCT_1:23
.= fa'bk + fb'ak by A10, A15, A23, FUNCT_1:23
.= (fa'b + fb'a) . k by A22, A23, VALUED_1:def 1 ; :: thesis:

end;

then fab' = fa'b + fb'a by FINSEQ_1:17;
hence TotDegree (a + b) = (TotDegree a) + (TotDegree b) by A3, A5, A7, A18, A19, A20, INTEGRA5:2; :: thesis: