let a, b, c, d be Real; :: thesis: 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)); :: thesis: ( 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 ) ; :: thesis: 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 ; :: thesis: 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)); :: thesis: for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy
let p, q, fx, fy be Real; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: 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 ; :: thesis: verum
end;
suppose A14: g | [.a,b.] is decreasing ; :: thesis: 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; :: thesis: verum
end;
end;