let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T
for X, Z being Subset of S st Z is open & Z c= X & f is_differentiable_on X holds
f `| Z = (f `| X) | Z
let f be PartFunc of S,T; :: thesis: for X, Z being Subset of S st Z is open & Z c= X & f is_differentiable_on X holds
f `| Z = (f `| X) | Z
let X, Z be Subset of S; :: 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
then A2: f is_differentiable_on Z by NDIFF_1:46;
then A3: dom (f `| Z) = Z by NDIFF_1:def 9;
A4: dom (f `| X) = X by A1, NDIFF_1:def 9;
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 ;
then reconsider x = x0 as Point of S ;
thus ((f `| X) | Z) . x0 = (f `| X) . x by A5, FUNCT_1:49
.= (f `| X) /. x by A1, A4, A6, PARTFUN1:def 6
.= diff (f,x) by A1, A6, NDIFF_1:def 9
.= (f `| Z) /. x by A2, A5, NDIFF_1:def 9
.= (f `| Z) . x0 by A3, A5, PARTFUN1:def 6 ; :: thesis: verum

end;

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