set g = R^1 f;

per cases
( not dom f is empty or dom f is empty )
;

end;

suppose
not dom f is empty
; :: thesis: 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

hence R^1 f is continuous by PRE_TOPC:27; :: thesis: verum

end;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

then
h is continuous
by TMAP_1:44;
let x be Point of (R^1 | (R^1 A)); :: thesis: h is_continuous_at x

let G be a_neighborhood of h . x; :: according to TMAP_1:def 2 :: thesis: ex b_{1} being a_neighborhood of x st h .: b_{1} 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 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 ; :: thesis: h .: M c= G

h .: M c= h .: NN by RELAT_1:123, XBOOLE_1:17;

then h .: M c= Z by A2;

hence h .: M c= G by A1; :: thesis: verum

end;let G be a_neighborhood of h . x; :: according to TMAP_1:def 2 :: thesis: ex b

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 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 ; :: thesis: h .: M c= G

h .: M c= h .: NN by RELAT_1:123, XBOOLE_1:17;

then h .: M c= Z by A2;

hence h .: M c= G by A1; :: thesis: verum

hence R^1 f is continuous by PRE_TOPC:27; :: thesis: verum