let a, b, d, e be Real; :: thesis:
assume that
A1: a <= b and
A2: e < 0 ; :: thesis:
set S = Closed-Interval-TSpace (a,b);
defpred S₁[ set , set ] 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:25;
then reconsider B = the carrier of (Closed-Interval-TSpace (a,b)) as Subset of R^1 by TOPMETR:24;
A4: R^1 | B = Closed-Interval-TSpace (a,b) by A1, A3, TOPMETR:26;
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:67;
then A6: the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) = [.((e * b) + d),((e * a) + d).] by TOPMETR:25, XREAL_1:9;
then reconsider C = the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) as Subset of R^1 by TOPMETR:24;
defpred S₂[ set , set ] 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 8;
then A7: Closed-Interval-TSpace (((e * b) + d),((e * a) + d)) is T_2 by PCOMPS_1:38;
A8: for x being set st x in the carrier of (Closed-Interval-TSpace (a,b)) holds
ex y being set st
( y in the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) & S₁[x,y] )

let x be set ; :: thesis:
assume A9: x in the carrier of (Closed-Interval-TSpace (a,b)) ; :: thesis:
then reconsider r1 = x as Real by A3;
set y1 = (e * r1) + d;
r1 <= b by A3, A9, XXREAL_1:1;
then e * r1 >= e * b by A2, XREAL_1:67;
then A10: (e * r1) + d >= (e * b) + d by XREAL_1:9;
a <= r1 by A3, A9, XXREAL_1:1;
then e * a >= e * r1 by A2, XREAL_1:67;
then (e * a) + d >= (e * r1) + d by XREAL_1:9;
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 set st
( y in the carrier of (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) & S₁[x,y] ) ; :: thesis:

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 set st x in the carrier of (Closed-Interval-TSpace (a,b)) holds
S₁[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 set st x in the carrier of (Closed-Interval-TSpace (a,b)) holds
S₁[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

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume A14: y in [#] (Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) ; :: thesis:
then reconsider ry = y as Real by A6;
ry <= (e * a) + d by A6, A14, XXREAL_1:1;
then ((e * a) + d) - d >= ry - d by XREAL_1:11;
then (a * e) / e <= (ry - d) / e by A2, XREAL_1:75;
then A15: a <= (ry - d) / e by A2, XCMPLX_1:90;
(e * b) + d <= ry by A6, A14, XXREAL_1:1;
then ((e * b) + d) - d <= ry - d by XREAL_1:11;
then (b * e) / e >= (ry - d) / e by A2, XREAL_1:75;
then b >= (ry - d) / e by A2, XCMPLX_1:90;
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:88
.= ry ;
hence y in rng f2 by A3, A13, A16, FUNCT_1:12; :: thesis:

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:4, TOPMETR:24;
for x1, x2 being set st x1 in dom f2 & x2 in dom f2 & f2 . x1 = f2 . x2 holds
x1 = x2

let x1, x2 be set ; :: thesis:
assume that
A18: x1 in dom f2 and
A19: x2 in dom f2 and
A20: f2 . x1 = f2 . x2 ; :: thesis:
reconsider r2 = x2 as Real by A3, A13, A19;
reconsider r1 = x1 as Real by A3, A13, 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:90;
hence x1 = x2 by A2, XCMPLX_1:90; :: thesis:

end;

let x be set ; :: thesis:
assume x in the carrier of R^1 ; :: thesis:
then reconsider rx = x as Real by TOPMETR:24;
reconsider ry = (e * rx) + d as Real ;
for r being Real st r = x holds
ry = (e * r) + d ;
hence ex y being set st
( y in the carrier of R^1 & S₂[x,y] ) by TOPMETR:24; :: thesis:

end;

ex f4 being Function of the carrier of R^1, the carrier of R^1 st
for x being set st x in the carrier of R^1 holds
S₂[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 set st x in the carrier of R^1 holds
S₂[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 A23, TOPMETR:24;
A25: (dom f5) /\ B = REAL /\ B by FUNCT_2:def 1, TOPMETR:24
.= B by TOPMETR:24, XBOOLE_1:28 ;
A26: for x being set st x in dom f3 holds
f3 . x = f5 . x

let x be set ; :: thesis:
assume A27: x in dom f3 ; :: thesis:
then reconsider rx = x as Real by A3, A13;
f4 . x = (e * rx) + d by A23, TOPMETR:24;
hence f3 . x = f5 . x by A11, A27; :: thesis:

end;