let a, b, c, d be Real; for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) st a < b & c < d & f is continuous & f is one-to-one & f . a = c & f . b = d holds
for x, y being Point of (Closed-Interval-TSpace (a,b))
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy
let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); ( a < b & c < d & f is continuous & f is one-to-one & f . a = c & f . b = d implies for x, y being Point of (Closed-Interval-TSpace (a,b))
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy )
assume that
A1:
a < b
and
A2:
c < d
and
A3:
( f is continuous & f is one-to-one )
and
A4:
( f . a = c & f . b = d )
; for x, y being Point of (Closed-Interval-TSpace (a,b))
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy
A5:
[.a,b.] = the carrier of (Closed-Interval-TSpace (a,b))
by A1, TOPMETR:18;
A6:
dom f = the carrier of (Closed-Interval-TSpace (a,b))
by FUNCT_2:def 1;
rng f c= REAL
by MEMBERED:3;
then reconsider g = f as PartFunc of [.a,b.],REAL by A5, A6, RELSET_1:4;
reconsider g = g as PartFunc of REAL,REAL by A5, A6, RELSET_1:5;
A7:
g | [.a,b.] is continuous
by A1, A2, A3, A4, Th14;
A8: [.a,b.] /\ (dom f) =
[.a,b.] /\ the carrier of (Closed-Interval-TSpace (a,b))
by FUNCT_2:def 1
.=
[.a,b.]
by A5
;
per cases
( g | [.a,b.] is increasing or g | [.a,b.] is decreasing )
by A1, A3, A8, A7, FCONT_2:17, XBOOLE_1:18;
suppose A9:
g | [.a,b.] is
increasing
;
for x, y being Point of (Closed-Interval-TSpace (a,b))
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy
for
x,
y being
Point of
(Closed-Interval-TSpace (a,b)) for
p,
q,
fx,
fy being
Real st
x = p &
y = q &
p < q &
fx = f . x &
fy = f . y holds
fx < fy
proof
let x,
y be
Point of
(Closed-Interval-TSpace (a,b));
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fylet p,
q,
fx,
fy be
Real;
( x = p & y = q & p < q & fx = f . x & fy = f . y implies fx < fy )
assume that A10:
x = p
and A11:
y = q
and A12:
(
p < q &
fx = f . x &
fy = f . y )
;
fx < fy
y in the
carrier of
(Closed-Interval-TSpace (a,b))
;
then A13:
q in [.a,b.] /\ (dom g)
by A1, A8, A11, TOPMETR:18;
x in the
carrier of
(Closed-Interval-TSpace (a,b))
;
then
p in [.a,b.] /\ (dom g)
by A1, A8, A10, TOPMETR:18;
hence
fx < fy
by A9, A10, A11, A12, A13, RFUNCT_2:20;
verum
end; hence
for
x,
y being
Point of
(Closed-Interval-TSpace (a,b)) for
p,
q,
fx,
fy being
Real st
x = p &
y = q &
p < q &
fx = f . x &
fy = f . y holds
fx < fy
;
verum end; suppose A14:
g | [.a,b.] is
decreasing
;
for x, y being Point of (Closed-Interval-TSpace (a,b))
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy
(
a in [.a,b.] /\ (dom g) &
b in [.a,b.] /\ (dom g) )
by A1, A5, A8, Lm6;
hence
for
x,
y being
Point of
(Closed-Interval-TSpace (a,b)) for
p,
q,
fx,
fy being
Real st
x = p &
y = q &
p < q &
fx = f . x &
fy = f . y holds
fx < fy
by A1, A2, A4, A14, RFUNCT_2:21;
verum end; end;