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;

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 <> {} )
;

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;

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;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 ) )

then A24:
b * xsbs9b = (len xsbs9b) |-> 0
by FUNCT_1:2;(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;(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

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