let a, b be Real; :: 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 ;
deffunc H₁( Real) -> Element of REAL = In ((((r2 - r1) * $1) + r1),REAL);
consider L being Function of REAL,REAL such that
A2: for r being Element of REAL holds L . r = H₁(r) from FUNCT_2:sch 4();
A3: for r being Real holds L . r = ((r2 - r1) * r) + r1

proof

let r be Real; :: thesis: L . r = ((r2 - r1) * r) + r1
reconsider r = r as Element of REAL by XREAL_0:def 1;
L . r = H₁(r) by A2;
hence L . r = ((r2 - r1) * r) + r1 ; :: thesis: verum

end;

reconsider f = L as Function of R^1,R^1 by TOPMETR:17;
A4: 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 ;
assume A5: s = w ; :: thesis: (L[01] (t1,t2)) . s = f . w
thus (L[01] (t1,t2)) . s = H₁(r) by A1, Th7
.= f . w by A3, A5 ; :: thesis: verum

end;

A6: [.0,1.] = the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18;
A7: f is continuous by A3, 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 A6, 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
A8: G0 is open and
A9: G0 /\ ([#] (Closed-Interval-TSpace (a,b))) = G by TOPS_2:24;
A10: f is_continuous_at w by A7, 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 A4;
then f . w in G0 by A9, XBOOLE_0:def 4;
then consider H0 being Subset of R^1 such that
A11: H0 is open and
A12: w in H0 and
A13: f .: H0 c= G0 by A8, A10, TMAP_1:43;

now :: 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 )

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 A11, TOPS_2:24; :: thesis: ( s in H & (L[01] (t1,t2)) .: H c= G )
thus s in H by A12, 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 object ; :: 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 object such that
r in dom (L[01] (t1,t2)) and
A14: r in H and
A15: t = (L[01] (t1,t2)) . r by FUNCT_1:def 6;
A16: r in the carrier of (Closed-Interval-TSpace (0,1)) by A14;
reconsider r = r as Point of (Closed-Interval-TSpace (0,1)) by A14;
r in dom (L[01] (t1,t2)) by A16, FUNCT_2:def 1;
then A17: t in (L[01] (t1,t2)) .: the carrier of (Closed-Interval-TSpace (0,1)) by A15, FUNCT_1:def 6;
reconsider p = r as Point of R^1 by A6, TARSKI:def 3, TOPMETR:17;
p in [#] R^1 ;
then A18: p in dom f by FUNCT_2:def 1;
( t = f . p & p in H0 ) by A4, A14, A15, XBOOLE_0:def 4;
then t in f .: H0 by A18, FUNCT_1:def 6;
hence t in G by A9, A13, A17, 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