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

proof

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

end;

reconsider f = P as Function of R^1,R^1 by TOPMETR:17;
A5: 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 ;
assume A6: 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, Th11
.= H₁(r)
.= f . w by A4, A6 ; :: thesis: verum

end;

A7: f is continuous by A4, 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
A8: G0 is open and
A9: G0 /\ ([#] (Closed-Interval-TSpace (0,1))) = G by TOPS_2:24;
A10: f is_continuous_at w by A7, 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 A5;
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 (a,b)) st
( H is open & s in H & (P[01] (a,b,t1,t2)) .: H c= G )

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 A11, TOPS_2:24; :: thesis: ( s in H & (P[01] (a,b,t1,t2)) .: H c= G )
thus s in H by A12, 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 object ; :: 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 object such that
r in dom (P[01] (a,b,t1,t2)) and
A14: r in H and
A15: t = (P[01] (a,b,t1,t2)) . r by FUNCT_1:def 6;
A16: r in the carrier of (Closed-Interval-TSpace (a,b)) by A14;
reconsider r = r as Point of (Closed-Interval-TSpace (a,b)) by A14;
r in dom (P[01] (a,b,t1,t2)) by A16, FUNCT_2:def 1;
then A17: t in (P[01] (a,b,t1,t2)) .: the carrier of (Closed-Interval-TSpace (a,b)) by A15, FUNCT_1:def 6;
reconsider p = r as Point of R^1 by A2, 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 A5, 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 (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