let A be closed-interval Subset of REAL; :: thesis: 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
let f be Function of A,REAL; :: thesis: ( f | A is bounded & f is integrable & not 0 in rng f & (f ^) | A is bounded implies f ^ is integrable )
assume that
A1: f | A is bounded and
A2: f is integrable and
A3: not 0 in rng f and
A4: (f ^) | A is bounded ; :: thesis: f ^ is integrable
consider r being real number such that
A5: for x being set st x in A /\ (dom (f ^)) holds
abs ((f ^) . x) <= r by A4, RFUNCT_1:90;
reconsider r = r as Real by XREAL_0:def 1;
f " {0} = {} by A3, FUNCT_1:142;
then A6: f ^ is total by RFUNCT_1:70;
A7: for x, y being Real st x in A & y in A holds
abs (((f ^) . x) - ((f ^) . y)) <= (r ^2) * (abs ((f . x) - (f . y)))

proof

let x, y be Real; :: thesis: ( x in A & y in A implies abs (((f ^) . x) - ((f ^) . y)) <= (r ^2) * (abs ((f . x) - (f . y))) )
assume that
A8: x in A and
A9: y in A ; :: thesis: abs (((f ^) . x) - ((f ^) . y)) <= (r ^2) * (abs ((f . x) - (f . y)))
A10: x in dom (f ^) by A6, A8, PARTFUN1:def 4;
then A11: f . x <> 0 by RFUNCT_1:13;
A12: y in dom (f ^) by A6, A9, PARTFUN1:def 4;
then A13: f . y <> 0 by RFUNCT_1:13;
( 0 <= 1 / (abs (f . x)) & 0 <= 1 / (abs (f . y)) & 1 / (abs (f . x)) <= r & 1 / (abs (f . y)) <= r )

proof

A14: abs (f . y) > 0 by A13, COMPLEX1:133;
abs (f . x) > 0 by A11, COMPLEX1:133;
hence ( 0 <= 1 / (abs (f . x)) & 0 <= 1 / (abs (f . y)) ) by A14; :: thesis: ( 1 / (abs (f . x)) <= r & 1 / (abs (f . y)) <= r )
reconsider x = x, y = y as Element of A by A8, A9;
y in A /\ (dom (f ^)) by A12, XBOOLE_0:def 4;
then abs ((f ^) . y) <= r by A5;
then abs (1 * ((f . y) ")) <= r by A12, RFUNCT_1:def 8;
then A15: abs (1 / (f . y)) <= r by XCMPLX_0:def 9;
x in A /\ (dom (f ^)) by A10, XBOOLE_0:def 4;
then abs ((f ^) . x) <= r by A5;
then abs (1 * ((f . x) ")) <= r by A10, RFUNCT_1:def 8;
then abs (1 / (f . x)) <= r by XCMPLX_0:def 9;
hence ( 1 / (abs (f . x)) <= r & 1 / (abs (f . y)) <= r ) by A15, ABSVALUE:15; :: thesis: verum

end;

then A16: (1 / (abs (f . x))) * (1 / (abs (f . y))) <= r * r by XREAL_1:68;
abs ((f . x) - (f . y)) >= 0 by COMPLEX1:132;
then A17: (abs ((f . x) - (f . y))) * ((1 / (abs (f . x))) * (1 / (abs (f . y)))) <= (abs ((f . x) - (f . y))) * (r ^2) by A16, XREAL_1:66;
((f ^) . x) - ((f ^) . y) = ((f . x) ") - ((f ^) . y) by A10, RFUNCT_1:def 8
.= ((f . x) ") - ((f . y) ") by A12, RFUNCT_1:def 8 ;
then abs (((f ^) . x) - ((f ^) . y)) = (abs ((f . x) - (f . y))) / ((abs (f . x)) * (abs (f . y))) by A13, A11, SEQ_2:11
.= ((abs ((f . x) - (f . y))) / (abs (f . x))) * (1 / (abs (f . y))) by XCMPLX_1:104
.= ((abs ((f . x) - (f . y))) * (1 / (abs (f . x)))) * (1 / (abs (f . y))) by XCMPLX_1:100 ;
hence abs (((f ^) . x) - ((f ^) . y)) <= (r ^2) * (abs ((f . x) - (f . y))) by A17; :: thesis: verum

end;

per cases ( r ^2 = 0 or r ^2 > 0 ) by XREAL_1:65;

suppose A18: r ^2 = 0 ; :: thesis: f ^ is integrable

for x, y being Real st x in A & y in A holds
abs (((f ^) . x) - ((f ^) . y)) <= 1 * (abs ((f . x) - (f . y)))

proof

let x, y be Real; :: thesis: ( x in A & y in A implies abs (((f ^) . x) - ((f ^) . y)) <= 1 * (abs ((f . x) - (f . y))) )
assume that
A19: x in A and
A20: y in A ; :: thesis: abs (((f ^) . x) - ((f ^) . y)) <= 1 * (abs ((f . x) - (f . y)))
abs (((f ^) . x) - ((f ^) . y)) <= 0 * (abs ((f . x) - (f . y))) by A7, A18, A19, A20;
hence abs (((f ^) . x) - ((f ^) . y)) <= 1 * (abs ((f . x) - (f . y))) by COMPLEX1:132; :: thesis: verum

end;

hence f ^ is integrable by A1, A2, A4, A6, Th27; :: thesis: verum

end;

suppose r ^2 > 0 ; :: thesis: f ^ is integrable

hence f ^ is integrable by A1, A2, A4, A6, A7, Th27; :: thesis: verum

end;

end;