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