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;
then A7: f ^ is Function of A,REAL ;
A8: 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 A9: ( x in A & y in A ) ; :: thesis: abs (((f ^ ) . x) - ((f ^ ) . y)) <= (r ^2 ) * (abs ((f . x) - (f . y)))
then A10: ( x in dom (f ^ ) & y in dom (f ^ ) ) by A6, PARTFUN1:def 4;
then A11: ((f ^ ) . x) - ((f ^ ) . y) = ((f . x) " ) - ((f ^ ) . y) by RFUNCT_1:def 8
.= ((f . x) " ) - ((f . y) " ) by A10, RFUNCT_1:def 8 ;
A12: ( f . x <> 0 & f . y <> 0 & abs (f . x) <> 0 & abs (f . y) <> 0 )

proof

thus ( f . x <> 0 & f . y <> 0 ) by A10, RFUNCT_1:13; :: thesis: ( abs (f . x) <> 0 & abs (f . y) <> 0 )
hence ( abs (f . x) <> 0 & abs (f . y) <> 0 ) by COMPLEX1:133; :: thesis: verum

end;

then A13: abs (((f ^ ) . x) - ((f ^ ) . y)) = (abs ((f . x) - (f . y))) / ((abs (f . x)) * (abs (f . y))) by 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 ;
A14: abs ((f . x) - (f . y)) >= 0 by COMPLEX1:132;
( 0 <= 1 / (abs (f . x)) & 0 <= 1 / (abs (f . y)) & 1 / (abs (f . x)) <= r & 1 / (abs (f . y)) <= r )

proof

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

end;

then (1 / (abs (f . x))) * (1 / (abs (f . y))) <= r * r by XREAL_1:68;
then (abs ((f . x) - (f . y))) * ((1 / (abs (f . x))) * (1 / (abs (f . y)))) <= (abs ((f . x) - (f . y))) * (r ^2 ) by A14, XREAL_1:66;
hence abs (((f ^ ) . x) - ((f ^ ) . y)) <= (r ^2 ) * (abs ((f . x) - (f . y))) by A13; :: thesis: verum

end;

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

suppose A15: 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 ( x in A & y in A ) ; :: thesis: abs (((f ^ ) . x) - ((f ^ ) . y)) <= 1 * (abs ((f . x) - (f . y)))
then abs (((f ^ ) . x) - ((f ^ ) . y)) <= 0 * (abs ((f . x) - (f . y))) by A8, A15;
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, A7, Th27; :: thesis: verum

end;

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

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

end;

end;