let a, b, c, d be Real; :: thesis: 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)); :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: ( x0 in dom (g | [.a,b.]) implies g | [.a,b.] is_continuous_in x0 )
assume x0 in dom (g | [.a,b.]) ; :: thesis: 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; :: thesis: verum
end;
hence g | [.a,b.] is continuous by FCONT_1:def 2; :: thesis: verum