let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f is_Rcontinuous_in x0 holds
f | (right_closed_halfline x0) is_continuous_in x0
let x0 be Real; :: thesis: ( f is_Rcontinuous_in x0 implies f | (right_closed_halfline x0) is_continuous_in x0 )
assume A1: f is_Rcontinuous_in x0 ; :: thesis: f | (right_closed_halfline x0) is_continuous_in x0
then A2: ( x0 in dom f & ( for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x being Real st x in dom f & x0 < x & x < x0 + d holds
|.((f . x) - (f . x0)).| < e ) ) ) ) by Th28;
set f1 = f | (right_closed_halfline x0);
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x being Real st x in dom (f | (right_closed_halfline x0)) & |.(x - x0).| < d holds
|.(((f | (right_closed_halfline x0)) . x) - ((f | (right_closed_halfline x0)) . x0)).| < e ) )

proof

let e be Real; :: thesis: ( 0 < e implies ex d being Real st
( 0 < d & ( for x being Real st x in dom (f | (right_closed_halfline x0)) & |.(x - x0).| < d holds
|.(((f | (right_closed_halfline x0)) . x) - ((f | (right_closed_halfline x0)) . x0)).| < e ) ) )
assume A3: 0 < e ; :: thesis: ex d being Real st
( 0 < d & ( for x being Real st x in dom (f | (right_closed_halfline x0)) & |.(x - x0).| < d holds
|.(((f | (right_closed_halfline x0)) . x) - ((f | (right_closed_halfline x0)) . x0)).| < e ) )
then consider d being Real such that
A4: 0 < d and
A5: for x being Real st x in dom f & x0 < x & x < x0 + d holds
|.((f . x) - (f . x0)).| < e by A1, Th28;
take d ; :: thesis: ( 0 < d & ( for x being Real st x in dom (f | (right_closed_halfline x0)) & |.(x - x0).| < d holds
|.(((f | (right_closed_halfline x0)) . x) - ((f | (right_closed_halfline x0)) . x0)).| < e ) )
thus 0 < d by A4; :: thesis: for x being Real st x in dom (f | (right_closed_halfline x0)) & |.(x - x0).| < d holds
|.(((f | (right_closed_halfline x0)) . x) - ((f | (right_closed_halfline x0)) . x0)).| < e
thus for x being Real st x in dom (f | (right_closed_halfline x0)) & |.(x - x0).| < d holds
|.(((f | (right_closed_halfline x0)) . x) - ((f | (right_closed_halfline x0)) . x0)).| < e :: thesis: verum

proof

let x be Real; :: thesis: ( x in dom (f | (right_closed_halfline x0)) & |.(x - x0).| < d implies |.(((f | (right_closed_halfline x0)) . x) - ((f | (right_closed_halfline x0)) . x0)).| < e )
assume that
A6: x in dom (f | (right_closed_halfline x0)) and
A7: |.(x - x0).| < d ; :: thesis: |.(((f | (right_closed_halfline x0)) . x) - ((f | (right_closed_halfline x0)) . x0)).| < e
dom (f | (right_closed_halfline x0)) = (dom f) /\ (right_closed_halfline x0) by RELAT_1:61;
then A8: ( x in dom f & x in right_closed_halfline x0 ) by A6, XBOOLE_0:def 4;
then x in [.x0,+infty.[ by LIMFUNC1:def 2;
then A9: x0 <= x by XXREAL_1:236;

per cases ( x = x0 or x <> x0 ) ;

suppose x = x0 ; :: thesis: |.(((f | (right_closed_halfline x0)) . x) - ((f | (right_closed_halfline x0)) . x0)).| < e

hence |.(((f | (right_closed_halfline x0)) . x) - ((f | (right_closed_halfline x0)) . x0)).| < e by A3, COMPLEX1:44; :: thesis: verum

end;

suppose x <> x0 ; :: thesis: |.(((f | (right_closed_halfline x0)) . x) - ((f | (right_closed_halfline x0)) . x0)).| < e

then A10: x0 < x by A9, XXREAL_0:1;
then x - x0 > 0 by XREAL_1:50;
then x - x0 < d by A7, ABSVALUE:def 1;
then A11: x < x0 + d by XREAL_1:19;
x0 in [.x0,+infty.[ by XXREAL_1:236;
then x0 in right_closed_halfline x0 by LIMFUNC1:def 2;
then ( (f | (right_closed_halfline x0)) . x = f . x & (f | (right_closed_halfline x0)) . x0 = f . x0 ) by A6, A2, RELAT_1:57, FUNCT_1:47;
hence |.(((f | (right_closed_halfline x0)) . x) - ((f | (right_closed_halfline x0)) . x0)).| < e by A5, A8, A10, A11; :: thesis: verum

end;

end;

end;

end;

hence f | (right_closed_halfline x0) is_continuous_in x0 by FCONT_1:3; :: thesis: verum