let n be Ordinal; :: thesis: for a, b being bag of n holds TotDegree (a + b) = (TotDegree a) + (TotDegree b)
let a, b be bag of n; :: thesis: TotDegree (a + b) = (TotDegree a) + (TotDegree b)
A1: field (RelIncl n) = n by WELLORD2:def 1;
A2: RelIncl n is being_linear-order by ORDERS_1:19;
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 fab9 = fab as FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;
set sasb = (support a) \/ (support b);
reconsider sasb = (support a) \/ (support b) as finite Subset of n ;
set s = SgmX ((RelIncl n),sasb);
set fa9b = a * (SgmX ((RelIncl n),sasb));
set fb9a = b * (SgmX ((RelIncl n),sasb));
RelIncl n linearly_orders sasb by A1, A2, ORDERS_1:37, ORDERS_1:38;
then A9: rng (SgmX ((RelIncl n),sasb)) = sasb by PRE_POLY:def 2;
A10: support (a + b) = sasb by PRE_POLY:38;
A11: dom a = n by PARTFUN1:def 2;
A12: dom b = n by PARTFUN1:def 2;
then reconsider fa9b = a * (SgmX ((RelIncl n),sasb)), fb9a = b * (SgmX ((RelIncl n),sasb)) as FinSequence by A9, A11, FINSEQ_1:16;
A13: rng fa9b c= rng a by RELAT_1:26;
A14: rng fb9a c= rng b by RELAT_1:26;
A15: rng fa9b c= NAT by VALUED_0:def 6;
A16: rng fb9a c= NAT by VALUED_0:def 6;
A17: rng fa9b c= REAL by A13, XBOOLE_1:1;
rng fb9a c= REAL by A14, XBOOLE_1:1;
then reconsider fa9b = fa9b, fb9a = fb9a as FinSequence of REAL by A17, FINSEQ_1:def 4;
reconsider fa9bn = fa9b, fb9an = fb9a as FinSequence of NAT by A15, A16, FINSEQ_1:def 4;
set ln = len fab;
A18: dom (a + b) = n by PARTFUN1:def 2;
A19: Seg (len fab) = dom fab by FINSEQ_1:def 3
.= dom (SgmX ((RelIncl n),sasb)) by A4, A9, A10, A18, RELAT_1:27 ;
then A20: Seg (len fab) = dom fa9b by A9, A11, RELAT_1:27;
A21: Seg (len fab) = dom fb9a by A9, A12, A19, RELAT_1:27;
A22: Sum fa = Sum fa9bn by A6, Th11;
A23: Sum fb = Sum fb9an by A8, Th11;
A24: len fa9b = len fb9a by A20, A21, FINSEQ_3:29;
then A25: len (fa9b + fb9a) = len fa9b by INTEGRA5:2;
then A26: Seg (len fab) = dom (fa9b + fb9a) by A20, FINSEQ_3:29;
reconsider fa9b9 = fa9b as natural-valued ManySortedSet of Seg (len fab) by A20, PARTFUN1:def 2, RELAT_1:def 18;

now :: thesis: ( Seg (len fab) = dom fab9 & Seg (len fab) = dom (fa9b + fb9a) & ( for k being Nat st k in Seg (len fab) holds
fab9 . k = (fa9b + fb9a) . k ) )

thus Seg (len fab) = dom fab9 by FINSEQ_1:def 3; :: thesis: ( Seg (len fab) = dom (fa9b + fb9a) & ( for k being Nat st k in Seg (len fab) holds
fab9 . k = (fa9b + fb9a) . k ) )
thus Seg (len fab) = dom (fa9b + fb9a) by A20, A25, FINSEQ_3:29; :: thesis: for k being Nat st k in Seg (len fab) holds
fab9 . k = (fa9b + fb9a) . k
let k be Nat; :: thesis: ( k in Seg (len fab) implies fab9 . k = (fa9b + fb9a) . k )
assume A27: k in Seg (len fab) ; :: thesis: fab9 . k = (fa9b + fb9a) . k
reconsider k1 = k as Nat ;
reconsider fa9bk = fa9b . k1, fb9ak = fb9a . k1 as Real ;
thus fab9 . k = (a + b) . ((SgmX ((RelIncl n),(support (a + b)))) . k) by A4, A10, A19, A27, FUNCT_1:13
.= (a . ((SgmX ((RelIncl n),(support (a + b)))) . k)) + (b . ((SgmX ((RelIncl n),(support (a + b)))) . k)) by PRE_POLY:def 5
.= (fa9b9 . k) + (b . ((SgmX ((RelIncl n),(support (a + b)))) . k)) by A10, A19, A27, FUNCT_1:13
.= fa9bk + fb9ak by A10, A19, A27, FUNCT_1:13
.= (fa9b + fb9a) . k by A26, A27, VALUED_1:def 1 ; :: thesis: verum

end;

then fab9 = fa9b + fb9a by FINSEQ_1:13;
hence TotDegree (a + b) = (TotDegree a) + (TotDegree b) by A3, A5, A7, A22, A23, A24, INTEGRA5:2; :: thesis: verum