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 A1: ( f is continuous & f is one-to-one & a < b & c < d & f = g & f . a = c & f . b = d ) ; :: thesis: g | [.a,b.] is continuous
for x0 being real number st x0 in dom (g | [.a,b.]) holds
g | [.a,b.] is_continuous_in x0

proof

let x0 be real number ; :: 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:86;
then reconsider x1 = x0 as Point of (Closed-Interval-TSpace a,b) by A1, TOPMETR:25;
A3: f is_continuous_at x1 by A1, TMAP_1:49;
x0 is Real by XREAL_0:def 1;
hence g | [.a,b.] is_continuous_in x0 by A1, A3, Th14; :: thesis: verum

end;

hence g | [.a,b.] is continuous by FCONT_1:def 2; :: thesis: verum