let A be non empty 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 such that
A5: for x being object st x in A /\ (dom (f ^)) holds
|.((f ^) . x).| <= r by A4, RFUNCT_1:73;
reconsider r = r as Real ;
f " {0} = {} by A3, FUNCT_1:72;
then A6: f ^ is total by RFUNCT_1:54;
A7: for x, y being Real st x in A & y in A holds
|.(((f ^) . x) - ((f ^) . y)).| <= (r ^2) * |.((f . x) - (f . y)).|

proof

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

proof

A14: |.(f . y).| > 0 by A13, COMPLEX1:47;
|.(f . x).| > 0 by A11, COMPLEX1:47;
hence ( 0 <= 1 / |.(f . x).| & 0 <= 1 / |.(f . y).| ) by A14; :: thesis: ( 1 / |.(f . x).| <= r & 1 / |.(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 |.((f ^) . y).| <= r by A5;
then |.(1 * ((f . y) ")).| <= r by A12, RFUNCT_1:def 2;
then A15: |.(1 / (f . y)).| <= r by XCMPLX_0:def 9;
x in A /\ (dom (f ^)) by A10, XBOOLE_0:def 4;
then |.((f ^) . x).| <= r by A5;
then |.(1 * ((f . x) ")).| <= r by A10, RFUNCT_1:def 2;
then |.(1 / (f . x)).| <= r by XCMPLX_0:def 9;
hence ( 1 / |.(f . x).| <= r & 1 / |.(f . y).| <= r ) by A15, ABSVALUE:7; :: thesis: verum

end;

then A16: (1 / |.(f . x).|) * (1 / |.(f . y).|) <= r * r by XREAL_1:66;
|.((f . x) - (f . y)).| >= 0 by COMPLEX1:46;
then A17: |.((f . x) - (f . y)).| * ((1 / |.(f . x).|) * (1 / |.(f . y).|)) <= |.((f . x) - (f . y)).| * (r ^2) by A16, XREAL_1:64;
((f ^) . x) - ((f ^) . y) = ((f . x) ") - ((f ^) . y) by A10, RFUNCT_1:def 2
.= ((f . x) ") - ((f . y) ") by A12, RFUNCT_1:def 2 ;
then |.(((f ^) . x) - ((f ^) . y)).| = |.((f . x) - (f . y)).| / (|.(f . x).| * |.(f . y).|) by A13, A11, SEQ_2:2
.= (|.((f . x) - (f . y)).| / |.(f . x).|) * (1 / |.(f . y).|) by XCMPLX_1:103
.= (|.((f . x) - (f . y)).| * (1 / |.(f . x).|)) * (1 / |.(f . y).|) by XCMPLX_1:99 ;
hence |.(((f ^) . x) - ((f ^) . y)).| <= (r ^2) * |.((f . x) - (f . y)).| by A17; :: thesis: verum

end;

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

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

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

proof

let x, y be Real; :: thesis: ( x in A & y in A implies |.(((f ^) . x) - ((f ^) . y)).| <= 1 * |.((f . x) - (f . y)).| )
assume that
A19: x in A and
A20: y in A ; :: thesis: |.(((f ^) . x) - ((f ^) . y)).| <= 1 * |.((f . x) - (f . y)).|
|.(((f ^) . x) - ((f ^) . y)).| <= 0 * |.((f . x) - (f . y)).| by A7, A18, A19, A20;
hence |.(((f ^) . x) - ((f ^) . y)).| <= 1 * |.((f . x) - (f . y)).| by COMPLEX1:46; :: 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;