theorem Th7: :: PDLAX:7

for f being PartFunc of REAL,REAL
for a, b being Real st a < b & ['a,b'] c= dom f & f | ['a,b'] is continuous holds
ex I being Real_Sequence st
( ( for n being Nat holds I . n = integral (f,(a + (1 / (n + 1))),(b - (1 / (n + 1)))) ) & I is convergent & lim I = integral (f,a,b) )