theorem Th51: :: INTEGRA1:53

for i being Element of NAT
for A being non empty closed_interval Subset of REAL
for D being Division of A
for f, g being Function of A,REAL st i in dom D & f | A is bounded_above & g | A is bounded_above holds
(upper_volume ((f + g),D)) . i <= ((upper_volume (f,D)) . i) + ((upper_volume (g,D)) . i)