let I be set ; :: thesis: for f being Function of I,NAT

for J, K being finite Subset of I st J misses K holds

Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K))

let f be Function of I,NAT; :: thesis: for J, K being finite Subset of I st J misses K holds

Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K))

let J, K be finite Subset of I; :: thesis: ( J misses K implies Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K)) )

assume A1: J misses K ; :: thesis: Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K))

for J, K being finite Subset of I st J misses K holds

Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K))

let f be Function of I,NAT; :: thesis: for J, K being finite Subset of I st J misses K holds

Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K))

let J, K be finite Subset of I; :: thesis: ( J misses K implies Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K)) )

assume A1: J misses K ; :: thesis: Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K))

per cases
( I is empty or not I is empty )
;

end;

suppose A2:
I is empty
; :: thesis: Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K))

set b = EmptyBag {};

A3: Sum (EmptyBag {}) = 0 by UPROOTS:11;

( J = {} & f | J = {} ) by A2;

hence Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K)) by A3; :: thesis: verum

end;A3: Sum (EmptyBag {}) = 0 by UPROOTS:11;

( J = {} & f | J = {} ) by A2;

hence Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K)) by A3; :: thesis: verum

suppose
not I is empty
; :: thesis: Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K))

then reconsider I9 = I as non empty set ;

[:I9,NAT:] c= [:I9,REAL:] by ZFMISC_1:95, NUMBERS:19;

then reconsider F = f as PartFunc of I9,REAL by XBOOLE_1:1;

A4: dom (F | (J \/ K)) is finite ;

thus Sum (f | (J \/ K)) = Sum (F,(J \/ K)) by Th25

.= (Sum (F,J)) + (Sum (F,K)) by A1, A4, RFUNCT_3:83

.= (Sum (f | J)) + (Sum (F,K)) by Th25

.= (Sum (f | J)) + (Sum (f | K)) by Th25 ; :: thesis: verum

end;[:I9,NAT:] c= [:I9,REAL:] by ZFMISC_1:95, NUMBERS:19;

then reconsider F = f as PartFunc of I9,REAL by XBOOLE_1:1;

A4: dom (F | (J \/ K)) is finite ;

thus Sum (f | (J \/ K)) = Sum (F,(J \/ K)) by Th25

.= (Sum (F,J)) + (Sum (F,K)) by A1, A4, RFUNCT_3:83

.= (Sum (f | J)) + (Sum (F,K)) by Th25

.= (Sum (f | J)) + (Sum (f | K)) by Th25 ; :: thesis: verum