let A be 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
let f be Function of A,REAL; ( 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
; 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;
( 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
;
|.(((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 )
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;
verum
end;