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

then A3: J = {} ;
A4: f | J = {} by A2;
set b = EmptyBag {} ;
A5: EmptyBag {} = {} --> 0 by POLYNOM1:def 15
.= {} ;
Sum (EmptyBag {} ) = 0 by UPROOTS:13;
hence Sum (f | (J \/ K)) = (Sum (f | J)) + (Sum (f | K)) by A3, A4, A5; :: thesis: verum

end;

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

then reconsider I' = I as non empty set ;
A6: [:I',NAT :] c= [:I',REAL :] by ZFMISC_1:118;
f c= [:I',REAL :] by A6, XBOOLE_1:1;
then reconsider F = f as PartFunc of I',REAL ;
A7: dom (F | (J \/ K)) is finite ;
thus Sum (f | (J \/ K)) = Sum F,(J \/ K) by Th25
.= (Sum F,J) + (Sum F,K) by A7, A1, RFUNCT_3:86
.= (Sum (f | J)) + (Sum F,K) by Th25
.= (Sum (f | J)) + (Sum (f | K)) by Th25 ; :: thesis: verum

end;

end;