let f be PartFunc of REAL,REAL; :: thesis: for I being Interval
for x being Real st f is_right_differentiable_in x & x in I & x <> sup I holds
f | I is_right_differentiable_in x
let I be Interval; :: thesis: for x being Real st f is_right_differentiable_in x & x in I & x <> sup I holds
f | I is_right_differentiable_in x
let x be Real; :: thesis: ( f is_right_differentiable_in x & x in I & x <> sup I implies f | I is_right_differentiable_in x )
assume that
A1: f is_right_differentiable_in x and
A2: x in I and
A3: x <> sup I ; :: thesis: f | I is_right_differentiable_in x
consider r being Real such that
A4: ( r > 0 & [.x,(x + r).] c= dom f ) by A1, FDIFF_3:def 3;
A5: x <= sup I by A2, XXREAL_2:4;
then A6: x < sup I by A3, XXREAL_0:1;
A7: x < +infty by XXREAL_0:9, XREAL_0:def 1;
-infty < sup I by A5, A2, XXREAL_0:2, XXREAL_0:12;
then A8: (sup I) - x > 0 by A6, A7, XXREAL_3:51;
set R0 = min (r,((sup I) - x));
A9: min (r,((sup I) - x)) > 0 by A4, A8, XXREAL_0:21;
A10: min (r,((sup I) - x)) <> -infty by A4, A8, XXREAL_0:21;
A11: ( min (r,((sup I) - x)) <= r & r < +infty ) by XREAL_0:def 1, XXREAL_0:17, XXREAL_0:9;
then min (r,((sup I) - x)) in REAL by A10, XXREAL_0:14;
then reconsider r0 = min (r,((sup I) - x)) as Real ;
set R = r0 / 2;
r0 > 0 by A4, A8, XXREAL_0:21;
then A12: r0 / 2 < r0 by XREAL_1:216;
then r0 / 2 < r by A11, XXREAL_0:2;
then x + (r0 / 2) < x + r by XREAL_1:6;
then [.x,(x + (r0 / 2)).] c= [.x,(x + r).] by XXREAL_1:34;
then A13: [.x,(x + (r0 / 2)).] 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;
A14: x in REAL by XREAL_0:def 1;
r0 <= (sup I) - x by XXREAL_0:17;
then r0 / 2 < (sup I) - x by A12, XXREAL_0:2;
then S + x0 < ((sup I) - x0) + x0 by A14, XXREAL_3:43;
then S + x0 < sup I by XXREAL_3:22;
then A15: x + (r0 / 2) < sup I by XXREAL_3:def 2;
A16: x < x + (r0 / 2) by A9, XREAL_1:29, XREAL_1:215;
then x + (r0 / 2) in I by A2, A15, XXREAL_2:81;
then [.x,(x + (r0 / 2)).] c= I by A2, XXREAL_2:def 12;
then [.x,(x + (r0 / 2)).] c= (dom f) /\ I by A13, XBOOLE_0:def 4;
then A17: [.x,(x + (r0 / 2)).] 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
A18: rng c = {x} and
A19: rng (h + c) c= dom (f | I) and
A20: 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 A19;
then A21: (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A1, A18, A20, FDIFF_3:def 3;
A22: (f | I) /* (h + c) = f /* (h + c) by A19, FUNCT_2:117;
[.x,(x + (r0 / 2)).] = (rng c) \/ ].x,(x + (r0 / 2)).] by A16, A18, XXREAL_1:130;
then rng c c= [.x,(x + (r0 / 2)).] by XBOOLE_1:7;
then rng c c= dom (f | I) by A17;
hence (h ") (#) (((f | I) /* (h + c)) - ((f | I) /* c)) is convergent by A22, A21, FUNCT_2:117; :: thesis: verum

end;

hence f | I is_right_differentiable_in x by A17, A9, XREAL_1:215, FDIFF_3:def 3; :: thesis: verum