let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f is_Lcontinuous_in x0 holds
f | (left_closed_halfline x0) is_continuous_in x0
let x0 be Real; :: thesis: ( f is_Lcontinuous_in x0 implies f | (left_closed_halfline x0) is_continuous_in x0 )
assume A1: f is_Lcontinuous_in x0 ; :: thesis: f | (left_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 - d < x & x < x0 holds
|.((f . x) - (f . x0)).| < e ) ) ) ) by Th27;
set f1 = f | (left_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 | (left_closed_halfline x0)) & |.(x - x0).| < d holds
|.(((f | (left_closed_halfline x0)) . x) - ((f | (left_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 | (left_closed_halfline x0)) & |.(x - x0).| < d holds
|.(((f | (left_closed_halfline x0)) . x) - ((f | (left_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 | (left_closed_halfline x0)) & |.(x - x0).| < d holds
|.(((f | (left_closed_halfline x0)) . x) - ((f | (left_closed_halfline x0)) . x0)).| < e ) )
consider d being Real such that
A4: 0 < d and
A5: for x being Real st x in dom f & x0 - d < x & x < x0 holds
|.((f . x) - (f . x0)).| < e by A1, A3, Th27;
take d ; :: thesis: ( 0 < d & ( for x being Real st x in dom (f | (left_closed_halfline x0)) & |.(x - x0).| < d holds
|.(((f | (left_closed_halfline x0)) . x) - ((f | (left_closed_halfline x0)) . x0)).| < e ) )
thus 0 < d by A4; :: thesis: for x being Real st x in dom (f | (left_closed_halfline x0)) & |.(x - x0).| < d holds
|.(((f | (left_closed_halfline x0)) . x) - ((f | (left_closed_halfline x0)) . x0)).| < e
thus for x being Real st x in dom (f | (left_closed_halfline x0)) & |.(x - x0).| < d holds
|.(((f | (left_closed_halfline x0)) . x) - ((f | (left_closed_halfline x0)) . x0)).| < e :: thesis: verum

proof

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

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

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

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

end;

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

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

end;

end;

end;

end;

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