theorem Th4: :: INTEGR19:4

for n being Element of NAT
for a, b, c, d being Real
for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds
['c,d'] c= dom (f + g)