let n be Ordinal; for a, b being bag of n holds TotDegree (a + b) = (TotDegree a) + (TotDegree b)
let a, b be bag of n; 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 ( 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;
( 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;
for k being Nat st k in Seg (len fab) holds
fab9 . k = (fa9b + fb9a) . klet k be
Nat;
( k in Seg (len fab) implies fab9 . k = (fa9b + fb9a) . k )assume A27:
k in Seg (len fab)
;
fab9 . k = (fa9b + fb9a) . kreconsider 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
;
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; verum