let X be open Subset of REAL; :: thesis: for f, F being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds
for x being Real st x in X holds
f is_continuous_in x
let f, F be PartFunc of REAL,REAL; :: thesis: ( X c= dom f & f | X is continuous implies for x being Real st x in X holds
f is_continuous_in x )
assume that
A1: X c= dom f and
A2: f | X is continuous ; :: thesis: for x being Real st x in X holds
f is_continuous_in x
A3: dom (f | X) = X by A1, RELAT_1:62;

hereby :: thesis: verum

let x be Real; :: thesis: ( x in X implies f is_continuous_in x )
assume A4: x in X ; :: thesis: f is_continuous_in x
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x).| < s holds
|.((f . x1) - (f . x)).| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x).| < s holds
|.((f . x1) - (f . x)).| < r ) ) )
consider ss1 being Real such that
A5: 0 < ss1 and
A6: ].(x - ss1),(x + ss1).[ c= X by A4, RCOMP_1:19;
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x).| < s holds
|.((f . x1) - (f . x)).| < r ) )
then consider s being Real such that
A7: 0 < s and
A8: for x1 being Real st x1 in dom (f | X) & |.(x1 - x).| < s holds
|.(((f | X) . x1) - ((f | X) . x)).| < r by A2, A4, A3, FCONT_1:def 2, FCONT_1:3;
set s1 = min (ss1,s);
take min (ss1,s) ; :: thesis: ( 0 < min (ss1,s) & ( for x1 being Real st x1 in dom f & |.(x1 - x).| < min (ss1,s) holds
|.((f . x1) - (f . x)).| < r ) )

now :: thesis: for x1 being Real st x1 in dom f & |.(x1 - x).| < min (ss1,s) holds
|.((f . x1) - (f . x)).| < r

let x1 be Real; :: thesis: ( x1 in dom f & |.(x1 - x).| < min (ss1,s) implies |.((f . x1) - (f . x)).| < r )
assume that
x1 in dom f and
A9: |.(x1 - x).| < min (ss1,s) ; :: thesis: |.((f . x1) - (f . x)).| < r
min (ss1,s) <= s by XXREAL_0:17;
then A10: |.(x1 - x).| < s by A9, XXREAL_0:2;
min (ss1,s) <= ss1 by XXREAL_0:17;
then |.(x1 - x).| < ss1 by A9, XXREAL_0:2;
then A11: x1 in ].(x - ss1),(x + ss1).[ by RCOMP_1:1;
then |.((f . x1) - (f . x)).| = |.(((f | X) . x1) - (f . x)).| by A6, A3, FUNCT_1:47;
then |.((f . x1) - (f . x)).| = |.(((f | X) . x1) - ((f | X) . x)).| by A4, A3, FUNCT_1:47;
hence |.((f . x1) - (f . x)).| < r by A8, A6, A10, A11, A3; :: thesis: verum

end;

hence ( 0 < min (ss1,s) & ( for x1 being Real st x1 in dom f & |.(x1 - x).| < min (ss1,s) holds
|.((f . x1) - (f . x)).| < r ) ) by A7, A5, XXREAL_0:15; :: thesis: verum

end;

hence f is_continuous_in x by FCONT_1:3; :: thesis: verum

end;