let f be PartFunc of REAL,REAL; :: thesis: for I being Interval
for x being Real st f is_left_differentiable_in x & x in I & x <> inf I holds
f | I is_left_differentiable_in x
let I be Interval; :: thesis: for x being Real st f is_left_differentiable_in x & x in I & x <> inf I holds
f | I is_left_differentiable_in x
let x be Real; :: thesis: ( f is_left_differentiable_in x & x in I & x <> inf I implies f | I is_left_differentiable_in x )
assume that
A1: f is_left_differentiable_in x and
A2: x in I and
A3: x <> inf I ; :: thesis: f | I is_left_differentiable_in x
consider r being Real such that
A4: ( r > 0 & [.(x - r),x.] c= dom f ) by A1, FDIFF_3:def 4;
A5: inf I <= x by A2, XXREAL_2:3;
then A6: inf I < x by A3, XXREAL_0:1;
A7: x in REAL by XREAL_0:def 1;
A8: -infty < x by XREAL_0:def 1, XXREAL_0:12;
inf I < +infty by A5, A7, XXREAL_0:2, XXREAL_0:9;
then A9: x - (inf I) > 0 by A6, A8, XXREAL_3:51;
set R0 = min (r,(x - (inf I)));
A10: min (r,(x - (inf I))) > 0 by A4, A9, XXREAL_0:21;
A11: min (r,(x - (inf I))) <> -infty by A4, A9, XXREAL_0:21;
A12: ( min (r,(x - (inf I))) <= r & r < +infty ) by XREAL_0:def 1, XXREAL_0:17, XXREAL_0:9;
then min (r,(x - (inf I))) in REAL by A11, XXREAL_0:14;
then reconsider r0 = min (r,(x - (inf I))) as Real ;
set R = r0 / 2;
A13: r0 / 2 < r0 by A10, XREAL_1:216;
then r0 / 2 < r by A12, XXREAL_0:2;
then x - r < x - (r0 / 2) by XREAL_1:10;
then [.(x - (r0 / 2)),x.] c= [.(x - r),x.] by XXREAL_1:34;
then A14: [.(x - (r0 / 2)),x.] c= dom f by A4;
reconsider x0 = x as R_eal by XXREAL_0:def 1;
reconsider S = r0 / 2 as R_eal by XXREAL_0:def 1;
A15: - S = - (r0 / 2) by XXREAL_3:def 3;
r0 <= x - (inf I) by XXREAL_0:17;
then r0 / 2 < x - (inf I) by A13, XXREAL_0:2;
then S - x0 < (x0 - (inf I)) - x0 by A7, XXREAL_3:43;
then S - x0 < ((- (inf I)) + x0) - x0 by XXREAL_3:def 4;
then S - x0 < - (inf I) by XXREAL_3:24;
then - (S - x0) > - (- (inf I)) by XXREAL_3:38;
then x0 + (- S) > inf I by XXREAL_3:26;
then A16: x - (r0 / 2) > inf I by A15, XXREAL_3:def 2;
A17: x - (r0 / 2) < x by A10, XREAL_1:44, XREAL_1:215;
then x - (r0 / 2) in I by A2, A16, XXREAL_2:82;
then [.(x - (r0 / 2)),x.] c= I by A2, XXREAL_2:def 12;
then [.(x - (r0 / 2)),x.] c= (dom f) /\ I by A14, XBOOLE_0:def 4;
then A18: [.(x - (r0 / 2)),x.] c= dom (f | I) by RELAT_1:61;
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x} & rng (h + c) c= dom (f | I) & ( for n being Nat holds h . n < 0 ) holds
(h ") (#) (((f | I) /* (h + c)) - ((f | I) /* c)) is convergent

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {x} & rng (h + c) c= dom (f | I) & ( for n being Nat holds h . n < 0 ) holds
(h ") (#) (((f | I) /* (h + c)) - ((f | I) /* c)) is convergent
let c be constant Real_Sequence; :: thesis: ( rng c = {x} & rng (h + c) c= dom (f | I) & ( for n being Nat holds h . n < 0 ) implies (h ") (#) (((f | I) /* (h + c)) - ((f | I) /* c)) is convergent )
assume that
A19: rng c = {x} and
A20: rng (h + c) c= dom (f | I) and
A21: for n being Nat holds h . n < 0 ; :: thesis: (h ") (#) (((f | I) /* (h + c)) - ((f | I) /* c)) is convergent
dom (f | I) c= dom f by RELAT_1:60;
then rng (h + c) c= dom f by A20;
then A22: (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A1, A19, A21, FDIFF_3:def 4;
A23: (f | I) /* (h + c) = f /* (h + c) by A20, FUNCT_2:117;
[.(x - (r0 / 2)),x.] = (rng c) \/ [.(x - (r0 / 2)),x.[ by A17, A19, XXREAL_1:129;
then rng c c= [.(x - (r0 / 2)),x.] by XBOOLE_1:7;
then rng c c= dom (f | I) by A18;
hence (h ") (#) (((f | I) /* (h + c)) - ((f | I) /* c)) is convergent by A23, A22, FUNCT_2:117; :: thesis: verum

end;

hence f | I is_left_differentiable_in x by A18, A10, XREAL_1:215, FDIFF_3:def 4; :: thesis: verum