set g = R^1 f;
per cases
( not dom f is empty or dom f is empty )
;
suppose
not
dom f is
empty
;
R^1 f is continuous then reconsider A =
dom f,
B =
rng f as non
empty Subset of
REAL by RELAT_1:42;
reconsider g =
R^1 f as
Function of
(R^1 | (R^1 A)),
(R^1 | (R^1 B)) ;
reconsider h =
g as
Function of
(R^1 | (R^1 A)),
R^1 by TOPREALA:7;
for
x being
Point of
(R^1 | (R^1 A)) holds
h is_continuous_at x
proof
let x be
Point of
(R^1 | (R^1 A));
h is_continuous_at xlet G be
a_neighborhood of
h . x;
TMAP_1:def 2 ex b1 being a_neighborhood of x st h .: b1 c= G
consider Z being
Neighbourhood of
f . x such that A1:
Z c= G
by TOPREALA:20;
reconsider xx =
x as
Point of
R^1 by PRE_TOPC:25;
the
carrier of
(R^1 | (R^1 A)) = A
by PRE_TOPC:8;
then
f is_continuous_in x
by FCONT_1:def 2;
then consider N being
Neighbourhood of
x such that A2:
f .: N c= Z
by FCONT_1:5;
consider g being
real number such that A3:
0 < g
and A4:
N = ].(x - g),(x + g).[
by RCOMP_1:def 6;
A5:
x + 0 < x + g
by A3, XREAL_1:6;
reconsider NN =
N as
open Subset of
R^1 by A4, JORDAN6:35, TOPMETR:17;
reconsider M =
NN /\ ([#] (R^1 | (R^1 A))) as
Subset of
(R^1 | (R^1 A)) ;
A6:
NN = Int NN
by TOPS_1:23;
x - g < x - 0
by A3, XREAL_1:15;
then
xx in Int NN
by A4, A6, A5, XXREAL_1:4;
then
NN is
open a_neighborhood of
xx
by CONNSP_2:def 1;
then reconsider M =
M as
open a_neighborhood of
x by TOPREALA:5;
take
M
;
h .: M c= G
h .: M c= h .: NN
by RELAT_1:123, XBOOLE_1:17;
then
h .: M c= Z
by A2, XBOOLE_1:1;
hence
h .: M c= G
by A1, XBOOLE_1:1;
verum
end; then
h is
continuous
by TMAP_1:44;
hence
R^1 f is
continuous
by PRE_TOPC:27;
verum end;