let a, b, c, d be Real; for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))
for g being PartFunc of REAL,REAL st f is continuous & f is one-to-one & a < b & c < d & f = g & f . a = c & f . b = d holds
g | [.a,b.] is continuous
let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); for g being PartFunc of REAL,REAL st f is continuous & f is one-to-one & a < b & c < d & f = g & f . a = c & f . b = d holds
g | [.a,b.] is continuous
let g be PartFunc of REAL,REAL; ( f is continuous & f is one-to-one & a < b & c < d & f = g & f . a = c & f . b = d implies g | [.a,b.] is continuous )
assume that
A1:
( f is continuous & f is one-to-one )
and
A2:
a < b
and
A3:
( c < d & f = g & f . a = c & f . b = d )
; g | [.a,b.] is continuous
for x0 being Real st x0 in dom (g | [.a,b.]) holds
g | [.a,b.] is_continuous_in x0
proof
let x0 be
Real;
( x0 in dom (g | [.a,b.]) implies g | [.a,b.] is_continuous_in x0 )
assume
x0 in dom (g | [.a,b.])
;
g | [.a,b.] is_continuous_in x0
then
x0 in [.a,b.]
by RELAT_1:57;
then reconsider x1 =
x0 as
Point of
(Closed-Interval-TSpace (a,b)) by A2, TOPMETR:18;
(
f is_continuous_at x1 &
x0 is
Real )
by A1, TMAP_1:44;
hence
g | [.a,b.] is_continuous_in x0
by A1, A2, A3, Th13;
verum
end;
hence
g | [.a,b.] is continuous
by FCONT_1:def 2; verum