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

now

let y be set ; :: 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:148;
then consider x being set such that
x in dom PI and
A5: x in [.a,b.] and
A6: y = PI . x by FUNCT_1:def 12;
reconsider c = x as Real by A5;
A7: d = (((b - c) * r1) + ((c - a) * r2)) / (b - a) 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:50;
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:155;
A13: 0 < b - a by A1, XREAL_1:52;
A14: 0 <= b - c by A9, XREAL_1:50;
then (b - c) * r1 <= b - c by A8, XREAL_1:155;
then ((b - c) * r1) + ((c - a) * r2) <= (b + (- c)) + (c - a) by A12, XREAL_1:9;
then d <= (b - a) / (b - a) by A13, A7, XREAL_1:74;
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, TARSKI:def 3;
A16: dom (PI | [.a,b.]) = (dom PI) /\ [.a,b.] by RELAT_1:90;
( [.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:25;
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:11;
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)
A19: s is Real by XREAL_0:def 1;
the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by A1, TOPMETR:25;
hence F . s = PI . s by FUNCT_1:72
.= (((b - s) * t1) + ((s - a) * t2)) / (b - a) by A2, A19 ;
:: thesis: verum