let a, b be real number ; :: thesis: ( a <= b implies for t1, t2 being Point of (Closed-Interval-TSpace a,b) holds L[01] t1,t2 is continuous Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace a,b) )
assume A1: a <= b ; :: thesis: for t1, t2 being Point of (Closed-Interval-TSpace a,b) holds L[01] t1,t2 is continuous Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace a,b)
let t1, t2 be Point of (Closed-Interval-TSpace a,b); :: thesis: L[01] t1,t2 is continuous Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace a,b)
reconsider r1 = t1, r2 = t2 as Real by A1, Lm2;
deffunc H₁( Element of REAL ) -> Element of REAL = ((r2 - r1) * $1) + r1;
consider L being Function of REAL ,REAL such that
A2: for r being Real holds L . r = H₁(r) from FUNCT_2:sch 4();
reconsider f = L as Function of R^1 ,R^1 by TOPMETR:24;
A3: for s being Point of (Closed-Interval-TSpace 0 ,1)
for w being Point of R^1 st s = w holds
(L[01] t1,t2) . s = f . w

proof

let s be Point of (Closed-Interval-TSpace 0 ,1); :: thesis: for w being Point of R^1 st s = w holds
(L[01] t1,t2) . s = f . w
let w be Point of R^1 ; :: thesis: ( s = w implies (L[01] t1,t2) . s = f . w )
reconsider r = s as Real by Lm2;
assume A4: s = w ; :: thesis: (L[01] t1,t2) . s = f . w
thus (L[01] t1,t2) . s = ((r2 - r1) * r) + r1 by A1, Th10
.= f . w by A2, A4 ; :: thesis: verum

end;

A5: [.0 ,1.] = the carrier of (Closed-Interval-TSpace 0 ,1) by TOPMETR:25;
A6: f is continuous by A2, TOPMETR:28;
for s being Point of (Closed-Interval-TSpace 0 ,1) holds L[01] t1,t2 is_continuous_at s

proof

let s be Point of (Closed-Interval-TSpace 0 ,1); :: thesis: L[01] t1,t2 is_continuous_at s
reconsider w = s as Point of R^1 by A5, TARSKI:def 3, TOPMETR:24;
for G being Subset of (Closed-Interval-TSpace a,b) st G is open & (L[01] t1,t2) . s in G holds
ex H being Subset of (Closed-Interval-TSpace 0 ,1) st
( H is open & s in H & (L[01] t1,t2) .: H c= G )

proof

let G be Subset of (Closed-Interval-TSpace a,b); :: thesis: ( G is open & (L[01] t1,t2) . s in G implies ex H being Subset of (Closed-Interval-TSpace 0 ,1) st
( H is open & s in H & (L[01] t1,t2) .: H c= G ) )
assume G is open ; :: thesis: ( not (L[01] t1,t2) . s in G or ex H being Subset of (Closed-Interval-TSpace 0 ,1) st
( H is open & s in H & (L[01] t1,t2) .: H c= G ) )
then consider G0 being Subset of R^1 such that
A7: G0 is open and
A8: G0 /\ ([#] (Closed-Interval-TSpace a,b)) = G by TOPS_2:32;
A9: f is_continuous_at w by A6, TMAP_1:49;
assume (L[01] t1,t2) . s in G ; :: thesis: ex H being Subset of (Closed-Interval-TSpace 0 ,1) st
( H is open & s in H & (L[01] t1,t2) .: H c= G )
then f . w in G by A3;
then f . w in G0 by A8, XBOOLE_0:def 4;
then consider H0 being Subset of R^1 such that
A10: H0 is open and
A11: w in H0 and
A12: f .: H0 c= G0 by A7, A9, TMAP_1:48;

now

reconsider H = H0 /\ ([#] (Closed-Interval-TSpace 0 ,1)) as Subset of (Closed-Interval-TSpace 0 ,1) ;
take H = H; :: thesis: ( H is open & s in H & (L[01] t1,t2) .: H c= G )
thus H is open by A10, TOPS_2:32; :: thesis: ( s in H & (L[01] t1,t2) .: H c= G )
thus s in H by A11, XBOOLE_0:def 4; :: thesis: (L[01] t1,t2) .: H c= G
thus (L[01] t1,t2) .: H c= G :: thesis: verum

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in (L[01] t1,t2) .: H or t in G )
assume t in (L[01] t1,t2) .: H ; :: thesis: t in G
then consider r being set such that
r in dom (L[01] t1,t2) and
A13: r in H and
A14: t = (L[01] t1,t2) . r by FUNCT_1:def 12;
A15: r in the carrier of (Closed-Interval-TSpace 0 ,1) by A13;
reconsider r = r as Point of (Closed-Interval-TSpace 0 ,1) by A13;
r in dom (L[01] t1,t2) by A15, FUNCT_2:def 1;
then A16: t in (L[01] t1,t2) .: the carrier of (Closed-Interval-TSpace 0 ,1) by A14, FUNCT_1:def 12;
reconsider p = r as Point of R^1 by A5, TARSKI:def 3, TOPMETR:24;
p in [#] R^1 ;
then A17: p in dom f by FUNCT_2:def 1;
( t = f . p & p in H0 ) by A3, A13, A14, XBOOLE_0:def 4;
then t in f .: H0 by A17, FUNCT_1:def 12;
hence t in G by A8, A12, A16, XBOOLE_0:def 4; :: thesis: verum

end;

end;

hence ex H being Subset of (Closed-Interval-TSpace 0 ,1) st
( H is open & s in H & (L[01] t1,t2) .: H c= G ) ; :: thesis: verum

end;

hence L[01] t1,t2 is_continuous_at s by TMAP_1:48; :: thesis: verum

end;

hence L[01] t1,t2 is continuous Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace a,b) by TMAP_1:49; :: thesis: verum