let n be Ordinal; :: thesis: for a, b being bag of n holds TotDegree (a + b) = () + ()
let a, b be bag of n; :: thesis: TotDegree (a + b) = () + ()
A1: field () = 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 ((),(support (a + b)))) by Def4;
consider fa being FinSequence of NAT such that
A5: TotDegree a = Sum fa and
A6: fa = a * (SgmX ((),())) by Def4;
consider fb being FinSequence of NAT such that
A7: TotDegree b = Sum fb and
A8: fb = b * (SgmX ((),())) by Def4;
reconsider fab9 = fab as FinSequence of REAL by ;
set sasb = () \/ ();
reconsider sasb = () \/ () as finite Subset of n ;
set s = SgmX ((),sasb);
set fa9b = a * (SgmX ((),sasb));
set fb9a = b * (SgmX ((),sasb));
RelIncl n linearly_orders sasb by ;
then A9: rng (SgmX ((),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 ((),sasb)), fb9a = b * (SgmX ((),sasb)) as FinSequence by ;
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 ;
rng fb9a c= REAL by ;
then reconsider fa9b = fa9b, fb9a = fb9a as FinSequence of REAL by ;
reconsider fa9bn = fa9b, fb9an = fb9a as FinSequence of NAT by ;
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 ((),sasb)) by ;
then A20: Seg (len fab) = dom fa9b by ;
A21: Seg (len fab) = dom fb9a by ;
A22: Sum fa = Sum fa9bn by ;
A23: Sum fb = Sum fb9an by ;
A24: len fa9b = len fb9a by ;
then A25: len (fa9b + fb9a) = len fa9b by INTEGRA5:2;
then A26: Seg (len fab) = dom (fa9b + fb9a) by ;
reconsider fa9b9 = fa9b as natural-valued ManySortedSet of Seg (len fab) by ;
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 ; :: 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 ((),(support (a + b)))) . k) by
.= (a . ((SgmX ((),(support (a + b)))) . k)) + (b . ((SgmX ((),(support (a + b)))) . k)) by PRE_POLY:def 5
.= (fa9b9 . k) + (b . ((SgmX ((),(support (a + b)))) . k)) by
.= fa9bk + fb9ak by
.= (fa9b + fb9a) . k by ; :: thesis: verum
end;
then fab9 = fa9b + fb9a by FINSEQ_1:13;
hence TotDegree (a + b) = () + () by ; :: thesis: verum