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;

hence TotDegree (a + b) = (TotDegree a) + (TotDegree b) by A3, A5, A7, A22, A23, A24, INTEGRA5:2; :: thesis: verum

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 ) )

then
fab9 = fa9b + fb9a
by FINSEQ_1:13;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;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

hence TotDegree (a + b) = (TotDegree a) + (TotDegree b) by A3, A5, A7, A22, A23, A24, INTEGRA5:2; :: thesis: verum