set g = R^1 f;

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

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

proof

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₁ being a_neighborhood of x st h .: b₁ 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;

then h is continuous by TMAP_1:44;
hence R^1 f is continuous by PRE_TOPC:27; :: thesis: verum

end;

suppose dom f is empty ; :: thesis: R^1 f is continuous

hence R^1 f is continuous ; :: thesis: verum

end;

end;