let a, b, d, e be Real; :: thesis: ( a <= b & e < 0 implies ex f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) st
( f is being_homeomorphism & ( for r being Real st r in [.a,b.] holds
f . r = (e * r) + d ) ) )
assume that
A1: a <= b and
A2: e < 0 ; :: thesis: ex f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) st
( f is being_homeomorphism & ( for r being Real st r in [.a,b.] holds
f . r = (e * r) + d ) )
set S = Closed-Interval-TSpace (a,b);
defpred S1[ object , object ] means for r being Real st $1 = r holds
$2 = (e * r) + d;
set X = the carrier of (Closed-Interval-TSpace (a,b));
A3: the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by A1, TOPMETR:18;
then reconsider B = the carrier of (Closed-Interval-TSpace (a,b)) as Subset of R^1 by TOPMETR:17;
A4: R^1 | B = Closed-Interval-TSpace (a,b) by A1, A3, TOPMETR:19;
set T = Closed-Interval-TSpace (((e * b) + d),((e * a) + d));
set Y = the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d)));
A5: e * a >= e * b by A1, A2, XREAL_1:65;
then A6: the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) = [.((e * b) + d),((e * a) + d).] by TOPMETR:18, XREAL_1:7;
then reconsider C = the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) as Subset of R^1 by TOPMETR:17;
defpred S2[ object , object ] means for r being Real st r = $1 holds
$2 = (e * r) + d;
Closed-Interval-TSpace (((e * b) + d),((e * a) + d)) = TopSpaceMetr (Closed-Interval-MSpace (((e * b) + d),((e * a) + d))) by TOPMETR:def 7;
then A7: Closed-Interval-TSpace (((e * b) + d),((e * a) + d)) is T_2 by PCOMPS_1:34;
A8: for x being object st x in the carrier of (Closed-Interval-TSpace (a,b)) holds
ex y being object st
( y in the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of (Closed-Interval-TSpace (a,b)) implies ex y being object st
( y in the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) & S1[x,y] ) )
assume A9: x in the carrier of (Closed-Interval-TSpace (a,b)) ; :: thesis: ex y being object st
( y in the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) & S1[x,y] )
then reconsider r1 = x as Real ;
set y1 = (e * r1) + d;
r1 <= b by A3, A9, XXREAL_1:1;
then e * r1 >= e * b by A2, XREAL_1:65;
then A10: (e * r1) + d >= (e * b) + d by XREAL_1:7;
a <= r1 by A3, A9, XXREAL_1:1;
then e * a >= e * r1 by A2, XREAL_1:65;
then (e * a) + d >= (e * r1) + d by XREAL_1:7;
then ( ( for r being Real st x = r holds
(e * r1) + d = (e * r) + d ) & (e * r1) + d in the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) ) by A6, A10, XXREAL_1:1;
hence ex y being object st
( y in the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) & S1[x,y] ) ; :: thesis: verum
end;
ex f being Function of the carrier of (Closed-Interval-TSpace (a,b)), the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) st
for x being object st x in the carrier of (Closed-Interval-TSpace (a,b)) holds
S1[x,f . x] from FUNCT_2:sch 1(A8);
 then consider f1 being Function of the carrier of (Closed-Interval-TSpace (a,b)), the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) such that
A11: for x being object st x in the carrier of (Closed-Interval-TSpace (a,b)) holds
S1[x,f1 . x] ;
reconsider f2 = f1 as Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) ;
A12: for r being Real st r in [.a,b.] holds
f2 . r = (e * r) + d by A3, A11;
A13: dom f2 = the carrier of (Closed-Interval-TSpace (a,b)) by FUNCT_2:def 1;
[#] (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) c= rng f2
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [#] (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) or y in rng f2 )
assume A14: y in [#] (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) ; :: thesis: y in rng f2
then reconsider ry = y as Real ;
ry <= (e * a) + d by A6, A14, XXREAL_1:1;
then ((e * a) + d) - d >= ry - d by XREAL_1:9;
then (a * e) / e <= (ry - d) / e by A2, XREAL_1:73;
then A15: a <= (ry - d) / e by A2, XCMPLX_1:89;
(e * b) + d <= ry by A6, A14, XXREAL_1:1;
then ((e * b) + d) - d <= ry - d by XREAL_1:9;
then (b * e) / e >= (ry - d) / e by A2, XREAL_1:73;
then b >= (ry - d) / e by A2, XCMPLX_1:89;
then A16: (ry - d) / e in [.a,b.] by A15, XXREAL_1:1;
then f2 . ((ry - d) / e) = (e * ((ry - d) / e)) + d by A3, A11
.= (ry - d) + d by A2, XCMPLX_1:87
.= ry ;
hence y in rng f2 by A3, A13, A16, FUNCT_1:3; :: thesis: verum
end;
then A17: rng f2 = [#] (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) by XBOOLE_0:def 10;
then reconsider f3 = f1 as Function of (Closed-Interval-TSpace (a,b)),R^1 by A6, A13, FUNCT_2:2, TOPMETR:17;
for x1, x2 being object st x1 in dom f2 & x2 in dom f2 & f2 . x1 = f2 . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in dom f2 & x2 in dom f2 & f2 . x1 = f2 . x2 implies x1 = x2 )
assume that
A18: x1 in dom f2 and
A19: x2 in dom f2 and
A20: f2 . x1 = f2 . x2 ; :: thesis: x1 = x2
reconsider r2 = x2 as Real by A19;
reconsider r1 = x1 as Real by A18;
f2 . x1 = (e * r1) + d by A11, A18;
then ((e * r1) + d) - d = ((e * r2) + d) - d by A11, A19, A20
.= e * r2 ;
then (r1 * e) / e = r2 by A2, XCMPLX_1:89;
hence x1 = x2 by A2, XCMPLX_1:89; :: thesis: verum
end;
then A21: ( dom f2 = [#] (Closed-Interval-TSpace (a,b)) & f2 is one-to-one ) by FUNCT_1:def 4, FUNCT_2:def 1;
A22: for x being object st x in the carrier of R^1 holds
ex y being object st
( y in the carrier of R^1 & S2[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of R^1 implies ex y being object st
( y in the carrier of R^1 & S2[x,y] ) )
assume x in the carrier of R^1 ; :: thesis: ex y being object st
( y in the carrier of R^1 & S2[x,y] )
then reconsider rx = x as Real ;
reconsider ry = (e * rx) + d as Element of REAL by XREAL_0:def 1;
for r being Real st r = x holds
ry = (e * r) + d ;
hence ex y being object st
( y in the carrier of R^1 & S2[x,y] ) by TOPMETR:17; :: thesis: verum
end;
ex f4 being Function of the carrier of R^1, the carrier of R^1 st
for x being object st x in the carrier of R^1 holds
S2[x,f4 . x] from FUNCT_2:sch 1(A22);
 then consider f4 being Function of the carrier of R^1, the carrier of R^1 such that
A23: for x being object st x in the carrier of R^1 holds
S2[x,f4 . x] ;
reconsider f5 = f4 as Function of R^1,R^1 ;
A24: for x being Real holds f5 . x = (e * x) + d by XREAL_0:def 1, TOPMETR:17, A23;
A25: (dom f5) /\ B = REAL /\ B by FUNCT_2:def 1, TOPMETR:17
.= B by TOPMETR:17, XBOOLE_1:28 ;
A26: for x being object st x in dom f3 holds
f3 . x = f5 . x
proof
let x be object ; :: thesis: ( x in dom f3 implies f3 . x = f5 . x )
assume A27: x in dom f3 ; :: thesis: f3 . x = f5 . x
then reconsider rx = x as Element of REAL by A3, A13;
f4 . x = (e * rx) + d by A23, TOPMETR:17;
hence f3 . x = f5 . x by A11, A27; :: thesis: verum
end;
dom f3 = B by FUNCT_2:def 1;
then f3 = f5 | B by A25, A26, FUNCT_1:46;
then A28: f3 is continuous by A24, A4, TOPMETR:7, TOPMETR:21;
A29: Closed-Interval-TSpace (a,b) is compact by A1, HEINE:4;
R^1 | C = Closed-Interval-TSpace (((e * b) + d),((e * a) + d)) by A5, A6, TOPMETR:19, XREAL_1:7;
then f2 is being_homeomorphism by A21, A17, A28, A29, A7, COMPTS_1:17, TOPMETR:6;
hence ex f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) st
( f is being_homeomorphism & ( for r being Real st r in [.a,b.] holds
f . r = (e * r) + d ) ) by A12; :: thesis: verum