reconsider a1 = a, b1 = b as Real ;
reconsider r1 = t1, r2 = t2 as Real ;
deffunc H₁( Real) -> Element of REAL = In (((((b1 - $1) * r1) + (($1 - a1) * r2)) / (b1 - a1)),REAL);
consider PI being Function of REAL,REAL such that
A2: for r being Element of REAL holds PI . r = H₁(r) from FUNCT_2:sch 4();
A3: [.0,1.] = the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18;

now :: thesis: for y being object st y in rng (PI | [.a,b.]) holds
y in [.0,1.]

let y be object ; :: thesis: ( y in rng (PI | [.a,b.]) implies y in [.0,1.] )
assume A4: y in rng (PI | [.a,b.]) ; :: thesis: y in [.0,1.]
then reconsider d = y as Real ;
y in PI .: [.a,b.] by A4, RELAT_1:115;
then consider x being object such that
x in dom PI and
A5: x in [.a,b.] and
A6: y = PI . x by FUNCT_1:def 6;
reconsider c = x as Element of REAL by A5;
A7: d = H₁(c) by A2, A6;
r1 in [.0,1.] by A3;
then r1 in { p where p is Real : ( 0 <= p & p <= 1 ) } by RCOMP_1:def 1;
then A8: ex v1 being Real st
( v1 = r1 & 0 <= v1 & v1 <= 1 ) ;
c in { p where p is Real : ( a <= p & p <= b ) } by A5, RCOMP_1:def 1;
then A9: ex u being Real st
( u = c & a <= u & u <= b ) ;
then A10: 0 <= c - a by XREAL_1:48;
r2 in [.0,1.] by A3;
then r2 in { p where p is Real : ( 0 <= p & p <= 1 ) } by RCOMP_1:def 1;
then A11: ex v2 being Real st
( v2 = r2 & 0 <= v2 & v2 <= 1 ) ;
then A12: (c - a) * r2 <= c - a by A10, XREAL_1:153;
A13: 0 < b - a by A1, XREAL_1:50;
A14: 0 <= b - c by A9, XREAL_1:48;
then (b - c) * r1 <= b - c by A8, XREAL_1:153;
then ((b - c) * r1) + ((c - a) * r2) <= (b + (- c)) + (c - a) by A12, XREAL_1:7;
then d <= (b - a) / (b - a) by A13, A7, XREAL_1:72;
then d <= 1 by A13, XCMPLX_1:60;
then y in { q where q is Real : ( 0 <= q & q <= 1 ) } by A8, A11, A13, A7, A14, A10;
hence y in [.0,1.] by RCOMP_1:def 1; :: thesis: verum

end;

then A15: rng (PI | [.a,b.]) c= the carrier of (Closed-Interval-TSpace (0,1)) by A3;
A16: dom (PI | [.a,b.]) = (dom PI) /\ [.a,b.] by RELAT_1:61;
( [.a,b.] = REAL /\ [.a,b.] & dom PI = REAL ) by FUNCT_2:def 1, XBOOLE_1:28;
then dom (PI | [.a,b.]) = the carrier of (Closed-Interval-TSpace (a,b)) by A1, A16, TOPMETR:18;
then reconsider F = PI | [.a,b.] as Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) by A15, FUNCT_2:def 1, RELSET_1:4;
take F ; :: thesis: for s being Point of (Closed-Interval-TSpace (a,b)) holds F . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a)
let s be Point of (Closed-Interval-TSpace (a,b)); :: thesis: F . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a)
A17: s in REAL by XREAL_0:def 1;
the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by A1, TOPMETR:18;
hence F . s = PI . s by FUNCT_1:49
.= H₁(s) by A2, A17
.= (((b - s) * t1) + ((s - a) * t2)) / (b - a) ;
:: thesis: verum