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 (RelIncl n),(support b)) & g = b * (SgmX (RelIncl n),((support b) \/ 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 (RelIncl n),(support b)) & g = b * (SgmX (RelIncl n),((support b) \/ 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 (RelIncl n),(support b)) & g = b * (SgmX (RelIncl n),((support b) \/ s)) holds
Sum f = Sum g
let f, g be FinSequence of NAT ; :: thesis: ( f = b * (SgmX (RelIncl n),(support b)) & g = b * (SgmX (RelIncl n),((support b) \/ s)) implies Sum f = Sum g )
assume that
A1: f = b * (SgmX (RelIncl n),(support b)) and
A2: g = b * (SgmX (RelIncl n),((support b) \/ s)) ; :: thesis: Sum f = Sum g
set sb = support b;
set sbs = (support b) \/ s;
set sbs9b = ((support b) \/ s) \ (support b);
set xsb = SgmX (RelIncl n),(support b);
set xsbs = SgmX (RelIncl n),((support b) \/ s);
set xsbs9b = SgmX (RelIncl n),(((support b) \/ s) \ (support b));
set xs = (SgmX (RelIncl n),(support b)) ^ (SgmX (RelIncl n),(((support b) \/ s) \ (support b)));
set h = b * ((SgmX (RelIncl n),(support b)) ^ (SgmX (RelIncl n),(((support b) \/ s) \ (support b))));
A3: dom b = n by PARTFUN1:def 4;
A4: field (RelIncl n) = n by WELLORD2:def 1;
A5: RelIncl n is well-ordering by WELLORD2:7;
then A6: RelIncl n is being_linear-order by ORDERS_1:107;
A7: RelIncl n linearly_orders n by A4, A5, ORDERS_1:107, ORDERS_1:133;
A8: RelIncl n linearly_orders (support b) \/ s by A4, A6, ORDERS_1:133, ORDERS_1:134;
A9: RelIncl n linearly_orders support b by A4, A6, ORDERS_1:133, ORDERS_1:134;
A10: RelIncl n linearly_orders ((support b) \/ s) \ (support b) by A4, A6, ORDERS_1:133, ORDERS_1:134;
A11: rng (SgmX (RelIncl n),((support b) \/ s)) = (support b) \/ s by A8, PRE_POLY:def 2;
A12: rng (SgmX (RelIncl n),(support b)) = support b by A9, PRE_POLY:def 2;
A13: rng (SgmX (RelIncl n),(((support b) \/ s) \ (support b))) = ((support b) \/ s) \ (support b) by A10, PRE_POLY:def 2;
then A14: rng ((SgmX (RelIncl n),(support b)) ^ (SgmX (RelIncl n),(((support b) \/ s) \ (support b)))) = (support b) \/ (((support b) \/ s) \ (support b)) by A12, FINSEQ_1:44;
then reconsider h = b * ((SgmX (RelIncl n),(support b)) ^ (SgmX (RelIncl n),(((support b) \/ s) \ (support b)))) as FinSequence by A3, FINSEQ_1:20;

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 (RelIncl n),(support b), xsbs9b = SgmX (RelIncl n),(((support b) \/ s) \ (support b)) as FinSequence of n ;
rng b c= REAL ;
then reconsider b = b as Function of n,REAL by A3, FUNCT_2:4;
rng h c= rng b by RELAT_1:45;
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 FINSEQ_2:27;
A15: support b misses ((support b) \/ s) \ (support b) by XBOOLE_1:79;
A16: (support b) \/ s = ((support b) \/ (support b)) \/ s
.= (support b) \/ ((support b) \/ s) by XBOOLE_1:4
.= (support b) \/ (((support b) \/ s) \ (support b)) by XBOOLE_1:39 ;
len ((SgmX (RelIncl n),(support b)) ^ (SgmX (RelIncl n),(((support b) \/ s) \ (support b)))) = (len xsb) + (len xsbs9b) by FINSEQ_1:35
.= (card (support b)) + (len xsbs9b) by A7, ORDERS_1:134, PRE_POLY:11
.= (card (support b)) + (card (((support b) \/ s) \ (support b))) by A7, ORDERS_1:134, PRE_POLY:11
.= card ((support b) \/ s) by A16, CARD_2:53, XBOOLE_1:79
.= len (SgmX (RelIncl n),((support b) \/ s)) by A7, ORDERS_1:134, PRE_POLY:11 ;
then A17: dom (SgmX (RelIncl n),((support b) \/ s)) = dom ((SgmX (RelIncl n),(support b)) ^ (SgmX (RelIncl n),(((support b) \/ s) \ (support b)))) by FINSEQ_3:31;
A18: SgmX (RelIncl n),((support b) \/ s) is one-to-one by A7, ORDERS_1:134, PRE_POLY:10;
A19: rng xsb = support b by A9, PRE_POLY:def 2;
A20: rng xsbs9b = ((support b) \/ s) \ (support b) by A10, PRE_POLY:def 2;
A21: xsb is one-to-one by A7, ORDERS_1:134, PRE_POLY:10;
xsbs9b is one-to-one by A7, ORDERS_1:134, PRE_POLY:10;
then (SgmX (RelIncl n),(support b)) ^ (SgmX (RelIncl n),(((support b) \/ s) \ (support b))) is one-to-one by A15, A19, A20, A21, FINSEQ_3:98;
then A22: gr,h are_fiberwise_equipotent by A2, A3, A11, A14, A16, A17, A18, Th4, RFINSEQ:39;

now

thus dom xsbs9b = dom (b * xsbs9b) by A3, A13, RELAT_1:46; :: thesis: ( dom xsbs9b = dom ((len xsbs9b) |-> 0 ) & ( for x being set st x in dom xsbs9b holds
(b * xsbs9b) . x = ((len xsbs9b) |-> 0 ) . x ) )
A23: dom xsbs9b = Seg (len xsbs9b) by FINSEQ_1:def 3;
hence dom xsbs9b = dom ((len xsbs9b) |-> 0 ) by FUNCOP_1:19; :: thesis: for x being set st x in dom xsbs9b holds
(b * xsbs9b) . x = ((len xsbs9b) |-> 0 ) . x
let x be set ; :: thesis: ( x in dom xsbs9b implies (b * xsbs9b) . x = ((len xsbs9b) |-> 0 ) . x )
assume A24: x in dom xsbs9b ; :: thesis: (b * xsbs9b) . x = ((len xsbs9b) |-> 0 ) . x
then xsbs9b . x in rng xsbs9b by FUNCT_1:12;
then not xsbs9b . x in support b by A13, XBOOLE_0:def 5;
then b . (xsbs9b . x) = 0 by PRE_POLY:def 7;
hence (b * xsbs9b) . x = 0 by A24, FUNCT_1:23
.= ((len xsbs9b) |-> 0 ) . x by A23, A24, FUNCOP_1:13 ;
:: thesis: verum

end;

then A25: b * xsbs9b = (len xsbs9b) |-> 0 by FUNCT_1:9;
h = (b * xsb) ^ (b * xsbs9b) by FINSEQOP:10;
then Sum h = (Sum (b * xsb)) + (Sum (b * xsbs9b)) by RVSUM_1:105
.= (Sum f) + 0 by A1, A25, RVSUM_1:111 ;
hence Sum f = Sum g by A22, RFINSEQ:22; :: thesis: verum

end;

end;