reconsider a1 = a, b1 = b as Real ;
reconsider r1 = t1, r2 = t2 as Real ;
deffunc H1( 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 = H1(r)
from FUNCT_2:sch 4();
A3:
[.0,1.] = the carrier of (Closed-Interval-TSpace (0,1))
by TOPMETR:18;
now for y being object st y in rng (PI | [.a,b.]) holds
y in [.0,1.]let y be
object ;
( y in rng (PI | [.a,b.]) implies y in [.0,1.] )assume A4:
y in rng (PI | [.a,b.])
;
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 = H1(
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;
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
; 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)); 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
.=
H1(s)
by A2, A17
.=
(((b - s) * t1) + ((s - a) * t2)) / (b - a)
;
verum