let f be PartFunc of REAL , REAL ; :: thesis: for A, B being 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 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
Z1: A c= dom f and
Z2: f | A is continuous and
Z3: B c= A ; :: thesis: f is_integrable_on B
X: B c= dom f by Z1, Z3, XBOOLE_1:1;
f | B is continuous by Z2, Z3, FCONT_1:17;
hence f is_integrable_on B by Th11, X; :: thesis: verum