reconsider r1 = t1, r2 = t2 as Element of REAL by A1, Lm2;
deffunc H1( 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 = H1(r)
from FUNCT_2:sch 4();
A3:
[.a,b.] = the carrier of (Closed-Interval-TSpace (a,b))
by A1, TOPMETR:18;
now for y being object st y in rng (LI | [.0,1.]) holds
y in [.a,b.]let y be
object ;
( y in rng (LI | [.0,1.]) implies y in [.a,b.] )assume A4:
y in rng (LI | [.0,1.])
;
y in [.a,b.]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 = H1(
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;
verum end;
then A15:
rng (LI | [.0,1.]) c= the carrier of (Closed-Interval-TSpace (a,b))
by A3;
A16:
dom (LI | [.0,1.]) = (dom LI) /\ [.0,1.]
by RELAT_1:61;
( [.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:18;
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:4;
take
F
; for s being Point of (Closed-Interval-TSpace (0,1)) holds F . s = ((1 - s) * t1) + (s * t2)
let s be Point of (Closed-Interval-TSpace (0,1)); F . s = ((1 - s) * t1) + (s * t2)
A17:
s in REAL
by XREAL_0:def 1;
the carrier of (Closed-Interval-TSpace (0,1)) = [.0,1.]
by TOPMETR:18;
hence F . s =
LI . s
by FUNCT_1:49
.=
H1(s)
by A2, A17
.=
((1 - s) * t1) + (s * t2)
;
verum