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

proof

let s be Point of (Closed-Interval-TSpace (a,b)); :: thesis: for w being Point of R^1 st s = w holds
(P[01] (a,b,t1,t2)) . s = f . w
let w be Point of R^1; :: thesis: ( s = w implies (P[01] (a,b,t1,t2)) . s = f . w )
reconsider r = s as Real by A1, Lm2;
assume A5: s = w ; :: thesis: (P[01] (a,b,t1,t2)) . s = f . w
thus (P[01] (a,b,t1,t2)) . s = (((r2 - r1) / (b - a)) * r) + (((b * r1) - (a * r2)) / (b - a)) by A1, Th14
.= f . w by A3, A5 ; :: thesis: verum

end;

A6: f is continuous by A3, TOPMETR:21;
for s being Point of (Closed-Interval-TSpace (a,b)) holds P[01] (a,b,t1,t2) is_continuous_at s

proof

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

proof

let G be Subset of (Closed-Interval-TSpace (0,1)); :: thesis: ( G is open & (P[01] (a,b,t1,t2)) . s in G implies ex H being Subset of (Closed-Interval-TSpace (a,b)) st
( H is open & s in H & (P[01] (a,b,t1,t2)) .: H c= G ) )
assume G is open ; :: thesis: ( not (P[01] (a,b,t1,t2)) . s in G or ex H being Subset of (Closed-Interval-TSpace (a,b)) st
( H is open & s in H & (P[01] (a,b,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 (0,1))) = G by TOPS_2:24;
A9: f is_continuous_at w by A6, TMAP_1:44;
assume (P[01] (a,b,t1,t2)) . s in G ; :: thesis: ex H being Subset of (Closed-Interval-TSpace (a,b)) st
( H is open & s in H & (P[01] (a,b,t1,t2)) .: H c= G )
then f . w in G by A4;
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 (a,b))) as Subset of (Closed-Interval-TSpace (a,b)) ;
take H = H; :: thesis: ( H is open & s in H & (P[01] (a,b,t1,t2)) .: H c= G )
thus H is open by A10, TOPS_2:24; :: thesis: ( s in H & (P[01] (a,b,t1,t2)) .: H c= G )
thus s in H by A11, XBOOLE_0:def 4; :: thesis: (P[01] (a,b,t1,t2)) .: H c= G
thus (P[01] (a,b,t1,t2)) .: H c= G :: thesis: verum

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in (P[01] (a,b,t1,t2)) .: H or t in G )
assume t in (P[01] (a,b,t1,t2)) .: H ; :: thesis: t in G
then consider r being set such that
r in dom (P[01] (a,b,t1,t2)) and
A13: r in H and
A14: t = (P[01] (a,b,t1,t2)) . r by FUNCT_1:def 6;
A15: r in the carrier of (Closed-Interval-TSpace (a,b)) by A13;
reconsider r = r as Point of (Closed-Interval-TSpace (a,b)) by A13;
r in dom (P[01] (a,b,t1,t2)) by A15, FUNCT_2:def 1;
then A16: t in (P[01] (a,b,t1,t2)) .: the carrier of (Closed-Interval-TSpace (a,b)) by A14, FUNCT_1:def 6;
reconsider p = r as Point of R^1 by A2, 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 A4, 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 (a,b)) st
( H is open & s in H & (P[01] (a,b,t1,t2)) .: H c= G ) ; :: thesis: verum

end;

hence P[01] (a,b,t1,t2) is_continuous_at s by TMAP_1:43; :: thesis: verum

end;

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