let x be Real; :: thesis: for f being PartFunc of REAL,REAL
for I being non empty Interval
for X being Subset of REAL st I c= X & x in I & x <> inf I holds
( f is_left_differentiable_in x iff f | X is_left_differentiable_in x )
let f be PartFunc of REAL,REAL; :: thesis: for I being non empty Interval
for X being Subset of REAL st I c= X & x in I & x <> inf I holds
( f is_left_differentiable_in x iff f | X is_left_differentiable_in x )
let I be non empty Interval; :: thesis: for X being Subset of REAL st I c= X & x in I & x <> inf I holds
( f is_left_differentiable_in x iff f | X is_left_differentiable_in x )
let X be Subset of REAL; :: thesis: ( I c= X & x in I & x <> inf I implies ( f is_left_differentiable_in x iff f | X is_left_differentiable_in x ) )
assume that
A1: I c= X and
A2: x in I and
A3: x <> inf I ; :: thesis: ( f is_left_differentiable_in x iff f | X is_left_differentiable_in x )
f | I c= f | X by A1, RELAT_1:75;
then A4: dom (f | I) c= dom (f | X) by RELAT_1:11;
A5: dom (f | X) c= dom f by RELAT_1:60;

hereby :: thesis: ( f | X is_left_differentiable_in x implies f is_left_differentiable_in x )

assume A6: f is_left_differentiable_in x ; :: thesis: f | X is_left_differentiable_in x
then f | I is_left_differentiable_in x by A2, A3, FDIFF_12:5;
then consider r being Real such that
A7: ( r > 0 & [.(x - r),x.] c= dom (f | I) ) by FDIFF_3:def 4;
A8: [.(x - r),x.] c= dom (f | X) by A4, A7;
x - r < x by A7, XREAL_1:44;
then A9: x in dom (f | X) by A8, XXREAL_1:1;
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 | X) & ( for n being Nat holds h . n < 0 ) holds
(h ") (#) (((f | X) /* (h + c)) - ((f | X) /* 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 | X) & ( for n being Nat holds h . n < 0 ) holds
(h ") (#) (((f | X) /* (h + c)) - ((f | X) /* c)) is convergent
let c be constant Real_Sequence; :: thesis: ( rng c = {x} & rng (h + c) c= dom (f | X) & ( for n being Nat holds h . n < 0 ) implies (h ") (#) (((f | X) /* (h + c)) - ((f | X) /* c)) is convergent )
assume that
A10: rng c = {x} and
A11: rng (h + c) c= dom (f | X) and
A12: for n being Nat holds h . n < 0 ; :: thesis: (h ") (#) (((f | X) /* (h + c)) - ((f | X) /* c)) is convergent
A13: ( (f | X) /* c = f /* c & (f | X) /* (h + c) = f /* (h + c) ) by A11, A9, A10, ZFMISC_1:31, FUNCT_2:117;
rng (h + c) c= dom f by A11, A5;
hence (h ") (#) (((f | X) /* (h + c)) - ((f | X) /* c)) is convergent by A13, A10, A12, A6, FDIFF_3:def 4; :: thesis: verum

end;

hence f | X is_left_differentiable_in x by A7, A8, FDIFF_3:def 4; :: thesis: verum

end;

assume f | X is_left_differentiable_in x ; :: thesis: f is_left_differentiable_in x
then (f | X) | I is_left_differentiable_in x by A2, A3, FDIFF_12:5;
then f | I is_left_differentiable_in x by A1, RELAT_1:74;
hence f is_left_differentiable_in x by FDIFF_12:10; :: thesis: verum