let f be PartFunc of REAL,REAL; :: thesis: for I being non empty Interval
for X being Subset of REAL st I c= X & f is_differentiable_on_interval I holds
f `\ I = (f | X) `\ I
let I be non empty Interval; :: thesis: for X being Subset of REAL st I c= X & f is_differentiable_on_interval I holds
f `\ I = (f | X) `\ I
let X be Subset of REAL; :: thesis: ( I c= X & f is_differentiable_on_interval I implies f `\ I = (f | X) `\ I )
assume that
A1: I c= X and
A2: f is_differentiable_on_interval I ; :: thesis: f `\ I = (f | X) `\ I
A3: f | X is_differentiable_on_interval I by A1, A2, Th15;
A4: f | I is_differentiable_on_interval I by A2, Th15;
A5: (f | X) | I is_differentiable_on_interval I by A3, Th15;
A6: ( dom (f `\ I) = I & dom ((f | X) `\ I) = I ) by A2, A3, FDIFF_12:def 2;

now :: thesis: for x being Element of REAL st x in dom (f `\ I) holds
(f `\ I) . x = ((f | X) `\ I) . x

let x be Element of REAL ; :: thesis: ( x in dom (f `\ I) implies (f `\ I) . b₁ = ((f | X) `\ I) . b<sub>1</sub> )
assume A7: x in dom (f `\ I) ; :: thesis: (f `\ I) . b<sub>1</sub> = ((f | X) `\ I) . b₁

per cases ( x = inf I or x = sup I or ( x <> inf I & x <> sup I ) ) ;

suppose A8: x = inf I ; :: thesis: (f `\ I) . b<sub>1</sub> = ((f | X) `\ I) . b₁

then A9: x = lower_bound I by A6, A7, Th1;
A10: f | I is_right_differentiable_in x by A4, A6, A7, A8, A9, FDIFF_12:def 1;
(f `\ I) . x = Rdiff (f,x) by A2, A6, A7, A8, FDIFF_12:def 2;
then A11: (f `\ I) . x = Rdiff ((f | I),x) by A10, FDIFF_12:9;
A12: (f | X) | I is_right_differentiable_in x by A5, A6, A7, A8, A9, FDIFF_12:def 1;
((f | X) `\ I) . x = Rdiff ((f | X),x) by A3, A6, A7, A8, FDIFF_12:def 2;
then ((f | X) `\ I) . x = Rdiff (((f | X) | I),x) by A12, FDIFF_12:9;
hence (f `\ I) . x = ((f | X) `\ I) . x by A11, A1, RELAT_1:74; :: thesis: verum

end;

suppose A13: x = sup I ; :: thesis: (f `\ I) . b<sub>1</sub> = ((f | X) `\ I) . b₁

then A14: x = upper_bound I by A6, A7, Th2;
A15: f | I is_left_differentiable_in x by A4, A6, A7, A13, A14, FDIFF_12:def 1;
(f `\ I) . x = Ldiff (f,x) by A2, A6, A7, A13, FDIFF_12:def 2;
then A16: (f `\ I) . x = Ldiff ((f | I),x) by A15, FDIFF_12:10;
A17: (f | X) | I is_left_differentiable_in x by A5, A6, A7, A13, A14, FDIFF_12:def 1;
((f | X) `\ I) . x = Ldiff ((f | X),x) by A3, A6, A7, A13, FDIFF_12:def 2;
then ((f | X) `\ I) . x = Ldiff (((f | X) | I),x) by A17, FDIFF_12:10;
hence (f `\ I) . x = ((f | X) `\ I) . x by A16, A1, RELAT_1:74; :: thesis: verum

end;

suppose A18: ( x <> inf I & x <> sup I ) ; :: thesis: (f `\ I) . b<sub>1</sub> = ((f | X) `\ I) . b₁

reconsider J = ].(inf I),(sup I).[ as open Subset of REAL by FDIFF_12:2;
J c= I by FDIFF_12:2;
then A19: J c= X by A1;
A20: x in J by A6, A7, A18, FDIFF_12:3;
f is_differentiable_on J by A2, FDIFF_12:def 1;
then f | J is_differentiable_in x by A6, A7, A18, FDIFF_12:3;
then f is_differentiable_in x by A20, PDIFFEQ1:2;
then A21: diff (f,x) = diff ((f | J),x) by A20, PDIFFEQ1:2;
f | X is_differentiable_on J by A3, FDIFF_12:def 1;
then (f | X) | J is_differentiable_in x by A6, A7, A18, FDIFF_12:3;
then f | X is_differentiable_in x by A20, PDIFFEQ1:2;
then diff ((f | X),x) = diff (((f | X) | J),x) by A20, PDIFFEQ1:2;
then A22: diff ((f | X),x) = diff ((f | J),x) by A19, RELAT_1:74;
(f `\ I) . x = diff (f,x) by A2, A6, A7, A18, FDIFF_12:def 2;
hence (f `\ I) . x = ((f | X) `\ I) . x by A21, A22, A3, A6, A7, A18, FDIFF_12:def 2; :: thesis: verum

end;

end;

end;

hence f `\ I = (f | X) `\ I by A6, PARTFUN1:5; :: thesis: verum