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

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

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;

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;

end;