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 )
assume A1: a <= b ; :: thesis: for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) holds L[01] (t1,t2) is continuous
let t1, t2 be Point of (Closed-Interval-TSpace (a,b)); :: thesis: L[01] (t1,t2) is continuous
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:17;
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:18;
A6: f is continuous by A2, TOPMETR:21;
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:17;
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:24;
A9: f is_continuous_at w by A6, TMAP_1:44;
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:43;

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:24; :: 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 6;
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 6;
reconsider p = r as Point of R^1 by A5, TARSKI:def 3, TOPMETR:17;
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 6;
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:43; :: thesis: verum

end;

hence L[01] (t1,t2) is continuous by TMAP_1:44; :: thesis: verum