for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded & f is integrable & not 0 in rng f & (f ^) | A is bounded holds
f ^ is integrable