let f be PartFunc of REAL,REAL; :: thesis: for A, B being non empty closed_interval Subset of REAL st A c= dom f & f | A is continuous & B c= A holds

f is_integrable_on B

let A, B be non empty closed_interval Subset of REAL; :: thesis: ( A c= dom f & f | A is continuous & B c= A implies f is_integrable_on B )

assume that

A1: A c= dom f and

A2: f | A is continuous and

A3: B c= A ; :: thesis: f is_integrable_on B

f | B is continuous by A2, A3, FCONT_1:16;

hence f is_integrable_on B by A1, A3, Th11, XBOOLE_1:1; :: thesis: verum

f is_integrable_on B

let A, B be non empty closed_interval Subset of REAL; :: thesis: ( A c= dom f & f | A is continuous & B c= A implies f is_integrable_on B )

assume that

A1: A c= dom f and

A2: f | A is continuous and

A3: B c= A ; :: thesis: f is_integrable_on B

f | B is continuous by A2, A3, FCONT_1:16;

hence f is_integrable_on B by A1, A3, Th11, XBOOLE_1:1; :: thesis: verum