let n be Ordinal; :: thesis: for b being bag of n
for s being finite Subset of n
for f, g being FinSequence of NAT st f = b * (SgmX ((),())) & g = b * (SgmX ((),(() \/ s))) holds
Sum f = Sum g

let b be bag of n; :: thesis: for s being finite Subset of n
for f, g being FinSequence of NAT st f = b * (SgmX ((),())) & g = b * (SgmX ((),(() \/ s))) holds
Sum f = Sum g

let s be finite Subset of n; :: thesis: for f, g being FinSequence of NAT st f = b * (SgmX ((),())) & g = b * (SgmX ((),(() \/ s))) holds
Sum f = Sum g

let f, g be FinSequence of NAT ; :: thesis: ( f = b * (SgmX ((),())) & g = b * (SgmX ((),(() \/ s))) implies Sum f = Sum g )
assume that
A1: f = b * (SgmX ((),())) and
A2: g = b * (SgmX ((),(() \/ s))) ; :: thesis: Sum f = Sum g
set sb = support b;
set sbs = () \/ s;
set sbs9b = (() \/ s) \ ();
set xsb = SgmX ((),());
set xsbs = SgmX ((),(() \/ s));
set xsbs9b = SgmX ((),((() \/ s) \ ()));
set xs = (SgmX ((),())) ^ (SgmX ((),((() \/ s) \ ())));
set h = b * ((SgmX ((),())) ^ (SgmX ((),((() \/ s) \ ()))));
A3: dom b = n by PARTFUN1:def 2;
A4: field () = n by WELLORD2:def 1;
A5: RelIncl n is being_linear-order by ORDERS_1:19;
A6: RelIncl n linearly_orders n by ;
A7: RelIncl n linearly_orders () \/ s by ;
A8: RelIncl n linearly_orders support b by ;
A9: RelIncl n linearly_orders (() \/ s) \ () by ;
A10: rng (SgmX ((),(() \/ s))) = () \/ s by ;
A11: rng (SgmX ((),())) = support b by ;
A12: rng (SgmX ((),((() \/ s) \ ()))) = (() \/ s) \ () by ;
then A13: rng ((SgmX ((),())) ^ (SgmX ((),((() \/ s) \ ())))) = () \/ ((() \/ s) \ ()) by ;
then reconsider h = b * ((SgmX ((),())) ^ (SgmX ((),((() \/ s) \ ())))) as FinSequence by ;
per cases ( n = {} or n <> {} ) ;
suppose n = {} ; :: thesis: Sum f = Sum g
hence Sum f = Sum g by A1, A2; :: thesis: verum
end;
suppose n <> {} ; :: thesis: Sum f = Sum g
then reconsider n = n as non empty Ordinal ;
reconsider xsb = SgmX ((),()), xsbs9b = SgmX ((),((() \/ s) \ ())) as FinSequence of n ;
rng b c= REAL ;
then reconsider b = b as Function of n,REAL by ;
rng h c= rng b by RELAT_1:26;
then rng h c= REAL by XBOOLE_1:1;
then reconsider h = h as FinSequence of REAL by FINSEQ_1:def 4;
reconsider gr = g as FinSequence of REAL by ;
A14: support b misses (() \/ s) \ () by XBOOLE_1:79;
A15: () \/ s = (() \/ ()) \/ s
.= () \/ (() \/ s) by XBOOLE_1:4
.= () \/ ((() \/ s) \ ()) by XBOOLE_1:39 ;
len ((SgmX ((),())) ^ (SgmX ((),((() \/ s) \ ())))) = (len xsb) + (len xsbs9b) by FINSEQ_1:22
.= (card ()) + (len xsbs9b) by
.= (card ()) + (card ((() \/ s) \ ())) by
.= card (() \/ s) by
.= len (SgmX ((),(() \/ s))) by ;
then A16: dom (SgmX ((),(() \/ s))) = dom ((SgmX ((),())) ^ (SgmX ((),((() \/ s) \ ())))) by FINSEQ_3:29;
A17: SgmX ((),(() \/ s)) is one-to-one by ;
A18: rng xsb = support b by ;
A19: rng xsbs9b = (() \/ s) \ () by ;
A20: xsb is one-to-one by ;
xsbs9b is one-to-one by ;
then (SgmX ((),())) ^ (SgmX ((),((() \/ s) \ ()))) is one-to-one by ;
then A21: gr,h are_fiberwise_equipotent by ;
now :: thesis: ( dom xsbs9b = dom (b * xsbs9b) & dom xsbs9b = dom ((len xsbs9b) |-> 0) & ( for x being object st x in dom xsbs9b holds
(b * xsbs9b) . x = ((len xsbs9b) |-> 0) . x ) )
thus dom xsbs9b = dom (b * xsbs9b) by ; :: thesis: ( dom xsbs9b = dom ((len xsbs9b) |-> 0) & ( for x being object st x in dom xsbs9b holds
(b * xsbs9b) . x = ((len xsbs9b) |-> 0) . x ) )

A22: dom xsbs9b = Seg (len xsbs9b) by FINSEQ_1:def 3;
hence dom xsbs9b = dom ((len xsbs9b) |-> 0) by FUNCOP_1:13; :: thesis: for x being object st x in dom xsbs9b holds
(b * xsbs9b) . x = ((len xsbs9b) |-> 0) . x

let x be object ; :: thesis: ( x in dom xsbs9b implies (b * xsbs9b) . x = ((len xsbs9b) |-> 0) . x )
assume A23: x in dom xsbs9b ; :: thesis: (b * xsbs9b) . x = ((len xsbs9b) |-> 0) . x
then xsbs9b . x in rng xsbs9b by FUNCT_1:3;
then not xsbs9b . x in support b by ;
then b . (xsbs9b . x) = 0 by PRE_POLY:def 7;
hence (b * xsbs9b) . x = 0 by
.= ((len xsbs9b) |-> 0) . x by ;
:: thesis: verum
end;
then A24: b * xsbs9b = (len xsbs9b) |-> 0 by FUNCT_1:2;
h = (b * xsb) ^ (b * xsbs9b) by FINSEQOP:9;
then Sum h = (Sum (b * xsb)) + (Sum (b * xsbs9b)) by RVSUM_1:75
.= (Sum f) + 0 by ;
hence Sum f = Sum g by ; :: thesis: verum
end;
end;