set g = R^1 f;
per cases ( not dom f is empty or dom f is empty ) ;
suppose not dom f is empty ; :: thesis:
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:
let G be a_neighborhood of h . x; :: according to TMAP_1:def 2 :: thesis: 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 such that
A3: 0 < g and
A4: N = ].(x - g),(x + g).[ by RCOMP_1:def 6;
A5: x + 0 < x + g by ;
reconsider NN = N as open Subset of R^1 by ;
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 ;
then xx in Int NN by ;
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 ;
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:
hence R^1 f is continuous ; :: thesis: verum
end;
end;