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

now

let y be set ; :: thesis: ( y in rng (LI | [.0 ,1.]) implies y in [.a,b.] )
assume A4: y in rng (LI | [.0 ,1.]) ; :: thesis: y in [.a,b.]
then reconsider d = y as Real ;
y in LI .: [.0 ,1.] by A4, RELAT_1:148;
then consider x being set such that
x in dom LI and
A5: x in [.0 ,1.] and
A6: y = LI . x by FUNCT_1:def 12;
reconsider c = x as Real by A5;
A7: d = ((1 - c) * r1) + (c * r2) by A2, A6;
r1 in [.a,b.] by A3;
then r1 in { p where p is Real : ( a <= p & p <= b ) } by RCOMP_1:def 1;
then A8: ex v1 being Real st
( v1 = r1 & a <= v1 & v1 <= b ) ;
c in { p where p is Real : ( 0 <= p & p <= 1 ) } by A5, RCOMP_1:def 1;
then A9: ex u being Real st
( u = c & 0 <= u & u <= 1 ) ;
r2 in [.a,b.] by A3;
then r2 in { p where p is Real : ( a <= p & p <= b ) } by RCOMP_1:def 1;
then A10: ex v2 being Real st
( v2 = r2 & a <= v2 & v2 <= b ) ;
then A11: c * a <= c * r2 by A9, XREAL_1:66;
A12: c * r2 <= c * b by A9, A10, XREAL_1:66;
A13: 0 <= 1 - c by A9, XREAL_1:50;
then (1 - c) * r1 <= (1 - c) * b by A8, XREAL_1:66;
then A14: d <= ((1 - c) * b) + (c * b) by A7, A12, XREAL_1:9;
(1 - c) * a <= (1 - c) * r1 by A8, A13, XREAL_1:66;
then ((1 - c) * a) + (c * a) <= d by A7, A11, XREAL_1:9;
then y in { q where q is Real : ( a <= q & q <= b ) } by A14;
hence y in [.a,b.] by RCOMP_1:def 1; :: thesis: verum

end;

then A15: rng (LI | [.0 ,1.]) c= the carrier of (Closed-Interval-TSpace a,b) by A3, TARSKI:def 3;
A16: dom (LI | [.0 ,1.]) = (dom LI) /\ [.0 ,1.] by RELAT_1:90;
( [.0 ,1.] = REAL /\ [.0 ,1.] & dom LI = REAL ) by FUNCT_2:def 1, XBOOLE_1:28;
then dom (LI | [.0 ,1.]) = the carrier of (Closed-Interval-TSpace 0 ,1) by A16, TOPMETR:25;
then reconsider F = LI | [.0 ,1.] as Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace a,b) by A15, FUNCT_2:def 1, RELSET_1:11;
take F ; :: thesis: for s being Point of (Closed-Interval-TSpace 0 ,1)
for r, r1, r2 being real number st s = r & r1 = t1 & r2 = t2 holds
F . s = ((1 - r) * r1) + (r * r2)
let s be Point of (Closed-Interval-TSpace 0 ,1); :: thesis: for r, r1, r2 being real number st s = r & r1 = t1 & r2 = t2 holds
F . s = ((1 - r) * r1) + (r * r2)
let r, r1, r2 be real number ; :: thesis: ( s = r & r1 = t1 & r2 = t2 implies F . s = ((1 - r) * r1) + (r * r2) )
assume that
A17: s = r and
A18: ( r1 = t1 & r2 = t2 ) ; :: thesis: F . s = ((1 - r) * r1) + (r * r2)
A19: r is Real by XREAL_0:def 1;
the carrier of (Closed-Interval-TSpace 0 ,1) = [.0 ,1.] by TOPMETR:25;
hence F . s = LI . r by A17, FUNCT_1:72
.= ((1 - r) * r1) + (r * r2) by A2, A18, A19 ;
:: thesis: verum