let f be PartFunc of REAL,REAL; :: thesis: for I, J being non empty Interval st f is_differentiable_on_interval I & J c= I & inf J < sup J holds
(f `\ I) | J = f `\ J
let I, J be non empty Interval; :: thesis: ( f is_differentiable_on_interval I & J c= I & inf J < sup J implies (f `\ I) | J = f `\ J )
assume that
A1: f is_differentiable_on_interval I and
A2: J c= I and
A3: inf J < sup J ; :: thesis: (f `\ I) | J = f `\ J
f is_differentiable_on_interval J by A1, A2, A3, FDIFF_12:38;
then A4: ( dom (f `\ I) = I & dom (f `\ J) = J ) by A1, FDIFF_12:def 2;
for x being Element of REAL st x in dom ((f `\ I) | J) holds
((f `\ I) | J) . x = (f `\ J) . x

proof

let x be Element of REAL ; :: thesis: ( x in dom ((f `\ I) | J) implies ((f `\ I) | J) . x = (f `\ J) . x )
assume A5: x in dom ((f `\ I) | J) ; :: thesis: ((f `\ I) | J) . x = (f `\ J) . x
then ((f `\ I) | J) . x = (f `\ I) . x by FUNCT_1:47;
hence ((f `\ I) | J) . x = (f `\ J) . x by A1, A2, A3, A5, FDIFF_12:38; :: thesis: verum

end;

hence (f `\ I) | J = f `\ J by A4, A2, RELAT_1:62, PARTFUN1:5; :: thesis: verum