let n be Ordinal; :: thesis: for b being bag of
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 ; :: 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 sbs'b = ((support b) \/ s) \ (support b);
set xsb = SgmX (RelIncl n),(support b);
set xsbs = SgmX (RelIncl n),((support b) \/ s);
set xsbs'b = 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;
B5: RelIncl n is well-ordering by WELLORD2:7;
then A5: RelIncl n is being_linear-order by ORDERS_1:107;
A6: RelIncl n linearly_orders n by A4, B5, ORDERS_1:107, ORDERS_1:133;
A7: RelIncl n linearly_orders (support b) \/ s by A4, A5, ORDERS_1:133, ORDERS_1:134;
A8: RelIncl n linearly_orders support b by A4, A5, ORDERS_1:133, ORDERS_1:134;
A9: RelIncl n linearly_orders ((support b) \/ s) \ (support b) by A4, A5, ORDERS_1:133, ORDERS_1:134;
A10: rng (SgmX (RelIncl n),((support b) \/ s)) = (support b) \/ s by A7, TRIANG_1:def 2;
A11: ( rng (SgmX (RelIncl n),(support b)) = support b & rng (SgmX (RelIncl n),(((support b) \/ s) \ (support b))) = ((support b) \/ s) \ (support b) ) by A8, A9, TRIANG_1:def 2;
then A12: rng ((SgmX (RelIncl n),(support b)) ^ (SgmX (RelIncl n),(((support b) \/ s) \ (support b)))) = (support b) \/ (((support b) \/ s) \ (support b)) by 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

then b = {} by A3;
then ( f = {} & g = {} ) by A1, A2;
hence Sum f = Sum g ; :: 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), xsbs'b = 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;
A13: support b misses ((support b) \/ s) \ (support b) by XBOOLE_1:79;
A14: (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 xsbs'b) by FINSEQ_1:35
.= (card (support b)) + (len xsbs'b) by A6, ORDERS_1:134, TRIANG_1:9
.= (card (support b)) + (card (((support b) \/ s) \ (support b))) by A6, ORDERS_1:134, TRIANG_1:9
.= card ((support b) \/ s) by A14, CARD_2:53, XBOOLE_1:79
.= len (SgmX (RelIncl n),((support b) \/ s)) by A6, ORDERS_1:134, TRIANG_1:9 ;
then A15: 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;
A16: SgmX (RelIncl n),((support b) \/ s) is one-to-one by A6, ORDERS_1:134, TRIANG_1:8;
A17: ( rng xsb = support b & rng xsbs'b = ((support b) \/ s) \ (support b) ) by A8, A9, TRIANG_1:def 2;
A18: xsb is one-to-one by A6, ORDERS_1:134, TRIANG_1:8;
xsbs'b is one-to-one by A6, ORDERS_1:134, TRIANG_1:8;
then (SgmX (RelIncl n),(support b)) ^ (SgmX (RelIncl n),(((support b) \/ s) \ (support b))) is one-to-one by A13, A17, A18, FINSEQ_3:98;
then A19: gr,h are_fiberwise_equipotent by A2, A3, A10, A12, A14, A15, A16, Th4, RFINSEQ:39;

now

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

end;

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

end;

end;