reconsider r1 = t1, r2 = t2 as Element of REAL by A1, Lm2;
deffunc H₁( Real) -> Element of REAL = In ((((1 - $1) * r1) + ($1 * r2)),REAL);
consider LI being Function of REAL,REAL such that
A2: for r being Element of 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:18;

let y be object ; :: thesis:
assume A4: y in rng (LI | [.0,1.]) ; :: thesis:
then reconsider d = y as Element of REAL ;
y in LI .: [.0,1.] by A4, RELAT_1:115;
then consider x being object such that
x in dom LI and
A5: x in [.0,1.] and
A6: y = LI . x by FUNCT_1:def 6;
reconsider c = x as Element of REAL by A5;
A7: d = H₁(c) 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:64;
A12: c * r2 <= c * b by A9, A10, XREAL_1:64;
A13: 0 <= 1 - c by A9, XREAL_1:48;
then (1 - c) * r1 <= (1 - c) * b by A8, XREAL_1:64;
then A14: d <= ((1 - c) * b) + (c * b) by A7, A12, XREAL_1:7;
(1 - c) * a <= (1 - c) * r1 by A8, A13, XREAL_1:64;
then ((1 - c) * a) + (c * a) <= d by A7, A11, XREAL_1:7;
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:

end;