let f be PartFunc of REAL,REAL; :: thesis: for X, Z being Subset of REAL st Z is open & Z c= X & f is_differentiable_on X holds
f `| Z = (f `| X) | Z
let X, Z be Subset of REAL; :: thesis: ( Z is open & Z c= X & f is_differentiable_on X implies f `| Z = (f `| X) | Z )
assume A1: ( Z is open & Z c= X & f is_differentiable_on X ) ; :: thesis: f `| Z = (f `| X) | Z
A2: f is_differentiable_on Z by A1, FDIFF_1:26;
then A3: dom (f `| Z) = Z by FDIFF_1:def 7;
A4: dom (f `| X) = X by A1, FDIFF_1:def 7;
for x being object st x in dom ((f `| X) | Z) holds
((f `| X) | Z) . x = (f `| Z) . x

proof

let x0 be object ; :: thesis: ( x0 in dom ((f `| X) | Z) implies ((f `| X) | Z) . x0 = (f `| Z) . x0 )
assume A5: x0 in dom ((f `| X) | Z) ; :: thesis: ((f `| X) | Z) . x0 = (f `| Z) . x0
then A6: x0 in Z ;
reconsider x = x0 as Real by A5;
thus ((f `| X) | Z) . x0 = (f `| X) . x by A5, FUNCT_1:49
.= diff (f,x) by A1, A6, FDIFF_1:def 7
.= (f `| Z) . x0 by A2, A5, FDIFF_1:def 7 ; :: thesis: verum

end;

hence f `| Z = (f `| X) | Z by A1, A3, A4, FUNCT_1:2, RELAT_1:62; :: thesis: verum