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 2;
A4: field (RelIncl n) = n by WELLORD2:def 1;
A5: RelIncl n is being_linear-order by ORDERS_1:19;
A6: RelIncl n linearly_orders n by A4, ORDERS_1:19, ORDERS_1:37;
A7: RelIncl n linearly_orders (support b) \/ s by A4, A5, ORDERS_1:37, ORDERS_1:38;
A8: RelIncl n linearly_orders support b by A4, A5, ORDERS_1:37, ORDERS_1:38;
A9: RelIncl n linearly_orders ((support b) \/ s) \ (support b) by A4, A5, ORDERS_1:37, ORDERS_1:38;
A10: rng (SgmX ((RelIncl n),((support b) \/ s))) = (support b) \/ s by A7, PRE_POLY:def 2;
A11: rng (SgmX ((RelIncl n),(support b))) = support b by A8, PRE_POLY:def 2;
A12: rng (SgmX ((RelIncl n),(((support b) \/ s) \ (support b)))) = ((support b) \/ s) \ (support b) by A9, PRE_POLY:def 2;
then A13: rng ((SgmX ((RelIncl n),(support b))) ^ (SgmX ((RelIncl n),(((support b) \/ s) \ (support b))))) = (support b) \/ (((support b) \/ s) \ (support b)) by A11, FINSEQ_1:31;
then reconsider h = b * ((SgmX ((RelIncl n),(support b))) ^ (SgmX ((RelIncl n),(((support b) \/ s) \ (support b))))) as FinSequence by A3, FINSEQ_1:16;

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:2;
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 FINSEQ_2:24, NUMBERS:19;
A14: support b misses ((support b) \/ s) \ (support b) by XBOOLE_1:79;
A15: (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:22
.= (card (support b)) + (len xsbs9b) by A6, ORDERS_1:38, PRE_POLY:11
.= (card (support b)) + (card (((support b) \/ s) \ (support b))) by A6, ORDERS_1:38, PRE_POLY:11
.= card ((support b) \/ s) by A15, CARD_2:40, XBOOLE_1:79
.= len (SgmX ((RelIncl n),((support b) \/ s))) by A6, ORDERS_1:38, PRE_POLY:11 ;
then A16: dom (SgmX ((RelIncl n),((support b) \/ s))) = dom ((SgmX ((RelIncl n),(support b))) ^ (SgmX ((RelIncl n),(((support b) \/ s) \ (support b))))) by FINSEQ_3:29;
A17: SgmX ((RelIncl n),((support b) \/ s)) is one-to-one by A6, ORDERS_1:38, PRE_POLY:10;
A18: rng xsb = support b by A8, PRE_POLY:def 2;
A19: rng xsbs9b = ((support b) \/ s) \ (support b) by A9, PRE_POLY:def 2;
A20: xsb is one-to-one by A6, ORDERS_1:38, PRE_POLY:10;
xsbs9b is one-to-one by A6, ORDERS_1:38, PRE_POLY:10;
then (SgmX ((RelIncl n),(support b))) ^ (SgmX ((RelIncl n),(((support b) \/ s) \ (support b)))) is one-to-one by A14, A18, A19, A20, FINSEQ_3:91;
then A21: gr,h are_fiberwise_equipotent by A2, A3, A10, A13, A15, A16, A17, CLASSES1:83, RFINSEQ:26;

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 A3, A12, RELAT_1:27; :: 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 A12, XBOOLE_0:def 5;
then b . (xsbs9b . x) = 0 by PRE_POLY:def 7;
hence (b * xsbs9b) . x = 0 by A23, FUNCT_1:13
.= ((len xsbs9b) |-> 0) . x by A22, A23, FUNCOP_1:7 ;
:: 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 A1, A24, RVSUM_1:81 ;
hence Sum f = Sum g by A21, RFINSEQ:9; :: thesis: verum

end;

end;