let a, b, c, d be Real; :: thesis:
let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); :: thesis:
let x be Point of (Closed-Interval-TSpace (a,b)); :: thesis:
let g be PartFunc of REAL,REAL; :: thesis:
let x1 be Real; :: thesis:
assume that
A1: a < b and
A2: c < d and
A3: f is_continuous_at x and
A4: x <> a and
A5: x <> b and
A6: f . a = c and
A7: f . b = d and
A8: f is one-to-one and
A9: f = g and
A10: x = x1 ; :: thesis:
A11: dom f = the carrier of (Closed-Interval-TSpace (a,b)) by FUNCT_2:def 1;
for N1 being Neighbourhood of g . x1 ex N being Neighbourhood of x1 st g .: N c= N1

reconsider fx = f . x as Point of (Closed-Interval-TSpace (c,d)) ;
set Rm = min (((g . x1) - c),(d - (g . x1)));
let N1 be Neighbourhood of g . x1; :: thesis:
Closed-Interval-TSpace (c,d) = TopSpaceMetr (Closed-Interval-MSpace (c,d)) by TOPMETR:def 7;
then A12: the topology of (Closed-Interval-TSpace (c,d)) = Family_open_set (Closed-Interval-MSpace (c,d)) by TOPMETR:12;
min (((g . x1) - c),(d - (g . x1))) > 0

A13: b in dom f by A1, A11, Lm6;
A14: a in dom f by A1, A11, Lm6;

per cases by XXREAL_0:15;

suppose A15: min (((g . x1) - c),(d - (g . x1))) = (g . x1) - c ; :: thesis:

g . x1 in the carrier of (Closed-Interval-TSpace (c,d)) by A9, A10, FUNCT_2:5;
then A16: g . x1 >= c by A2, Lm6;
min (((g . x1) - c),(d - (g . x1))) <> 0 by A4, A6, A8, A9, A10, A11, A14, A15, FUNCT_1:def 4;
hence min (((g . x1) - c),(d - (g . x1))) > 0 by A15, A16, XREAL_1:48; :: thesis:

end;

suppose A17: min (((g . x1) - c),(d - (g . x1))) = d - (g . x1) ; :: thesis:

g . x1 in the carrier of (Closed-Interval-TSpace (c,d)) by A9, A10, FUNCT_2:5;
then A18: g . x1 <= d by A2, Lm6;
d - (g . x1) <> d - d by A5, A7, A8, A9, A10, A11, A13, FUNCT_1:def 4;
hence min (((g . x1) - c),(d - (g . x1))) > 0 by A17, A18, XREAL_1:48; :: thesis:

end;

end;

end;

then reconsider Wuj = ].((g . x1) - (min (((g . x1) - c),(d - (g . x1))))),((g . x1) + (min (((g . x1) - c),(d - (g . x1))))).[ as Neighbourhood of g . x1 by RCOMP_1:def 6;
consider Ham being Neighbourhood of g . x1 such that
A19: Ham c= N1 and
A20: Ham c= Wuj by RCOMP_1:17;
A21: Wuj c= ].c,d.[

let aa be object ; :: according to TARSKI:def 3 :: thesis:
assume aa in Wuj ; :: thesis:
then aa in { l where l is Real : ( (g . x1) - (min (((g . x1) - c),(d - (g . x1)))) < l & l < (g . x1) + (min (((g . x1) - c),(d - (g . x1)))) ) } by RCOMP_1:def 2;
then consider A being Real such that
A22: A = aa and
A23: (g . x1) - (min (((g . x1) - c),(d - (g . x1)))) < A and
A24: A < (g . x1) + (min (((g . x1) - c),(d - (g . x1)))) ;
min (((g . x1) - c),(d - (g . x1))) <= d - (g . x1) by XXREAL_0:17;
then (g . x1) + (min (((g . x1) - c),(d - (g . x1)))) <= (g . x1) + (d - (g . x1)) by XREAL_1:6;
then A25: A < d by A24, XXREAL_0:2;
min (((g . x1) - c),(d - (g . x1))) <= (g . x1) - c by XXREAL_0:17;
then c + (min (((g . x1) - c),(d - (g . x1)))) <= g . x1 by XREAL_1:19;
then c <= (g . x1) - (min (((g . x1) - c),(d - (g . x1)))) by XREAL_1:19;
then c < A by A23, XXREAL_0:2;
then A in { l where l is Real : ( c < l & l < d ) } by A25;
hence aa in ].c,d.[ by A22, RCOMP_1:def 2; :: thesis:

end;

].c,d.[ c= [.c,d.] by XXREAL_1:25;
then A26: Wuj c= [.c,d.] by A21;
then Wuj c= the carrier of (Closed-Interval-MSpace (c,d)) by A2, TOPMETR:10;
then reconsider N21 = Ham as Subset of (Closed-Interval-MSpace (c,d)) by A20, XBOOLE_1:1;
the carrier of (Closed-Interval-MSpace (c,d)) = the carrier of (TopSpaceMetr (Closed-Interval-MSpace (c,d))) by TOPMETR:12
.= the carrier of (Closed-Interval-TSpace (c,d)) by TOPMETR:def 7 ;
then reconsider N19 = N21 as Subset of (Closed-Interval-TSpace (c,d)) ;
N21 in Family_open_set (Closed-Interval-MSpace (c,d)) by Th12;
then N19 is open by A12;
then reconsider G = N19 as a_neighborhood of fx by A9, A10, CONNSP_2:3, RCOMP_1:16;
consider H being a_neighborhood of x such that
A27: f .: H c= G by A3, TMAP_1:def 2;
consider V being Subset of (Closed-Interval-TSpace (a,b)) such that
A28: V is open and
A29: V c= H and
A30: x in V by CONNSP_2:6;
A31: the carrier of (Closed-Interval-MSpace (a,b)) = the carrier of (TopSpaceMetr (Closed-Interval-MSpace (a,b))) by TOPMETR:12
.= the carrier of (Closed-Interval-TSpace (a,b)) by TOPMETR:def 7 ;
then reconsider V2 = V as Subset of (Closed-Interval-MSpace (a,b)) ;
V c= the carrier of (Closed-Interval-MSpace (a,b)) by A31;
then V c= [.a,b.] by A1, TOPMETR:10;
then reconsider V1 = V as Subset of REAL by XBOOLE_1:1;
A32: Ham c= [.c,d.] by A20, A26;
A33: ( not a in V1 & not b in V1 )

assume A34: ( a in V1 or b in V1 ) ; :: thesis:

per cases by A34;

suppose a in V1 ; :: thesis:

then f . a in f .: H by A11, A29, FUNCT_1:def 6;
hence contradiction by A6, A32, A27, Th11; :: thesis:

end;

suppose b in V1 ; :: thesis:

then f . b in f .: H by A11, A29, FUNCT_1:def 6;
hence contradiction by A7, A32, A27, Th11; :: thesis:

end;

end;

end;

Closed-Interval-TSpace (a,b) = TopSpaceMetr (Closed-Interval-MSpace (a,b)) by TOPMETR:def 7;
then the topology of (Closed-Interval-TSpace (a,b)) = Family_open_set (Closed-Interval-MSpace (a,b)) by TOPMETR:12;
then V2 in Family_open_set (Closed-Interval-MSpace (a,b)) by A28;
then V1 is open by A1, A33, Th10;
then consider N being Neighbourhood of x1 such that
A35: N c= V1 by A10, A30, RCOMP_1:18;
N c= H by A29, A35;
then A36: g .: N c= g .: H by RELAT_1:123;
f .: H c= N1 by A19, A27;
hence ex N being Neighbourhood of x1 st g .: N c= N1 by A9, A36, XBOOLE_1:1; :: thesis:

end;

hence g is_continuous_in x1 by FCONT_1:5; :: thesis: