let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T
for Z being Subset of S st f is_differentiable_on Z holds
(f | Z) `| Z = f `| Z
let f be PartFunc of S,T; :: thesis: for Z being Subset of S st f is_differentiable_on Z holds
(f | Z) `| Z = f `| Z
let Z be Subset of S; :: thesis: ( f is_differentiable_on Z implies (f | Z) `| Z = f `| Z )
assume A1: f is_differentiable_on Z ; :: thesis: (f | Z) `| Z = f `| Z
then A2: f | Z is_differentiable_on Z by Th3;
A3: dom (f `| Z) = Z by A1, NDIFF_1:def 9;
A4: dom ((f | Z) `| Z) = Z by A2, NDIFF_1:def 9;
A5: Z is open by A1, NDIFF_1:32;

now :: thesis: for x being object st x in dom ((f | Z) `| Z) holds
((f | Z) `| Z) . x = (f `| Z) . x

let x be object ; :: thesis: ( x in dom ((f | Z) `| Z) implies ((f | Z) `| Z) . x = (f `| Z) . x )
assume A6: x in dom ((f | Z) `| Z) ; :: thesis: ((f | Z) `| Z) . x = (f `| Z) . x
then reconsider x0 = x as Point of S ;
A7: f is_differentiable_in x0 by A1, A4, A5, A6, NDIFF_1:31;
thus ((f | Z) `| Z) . x = ((f | Z) `| Z) /. x0 by A6, PARTFUN1:def 6
.= diff ((f | Z),x0) by A2, A4, A6, NDIFF_1:def 9
.= diff (f,x0) by A1, A4, A5, A6, A7, NDIFF_9:1
.= (f `| Z) /. x by A1, A4, A6, NDIFF_1:def 9
.= (f `| Z) . x by A3, A4, A6, PARTFUN1:def 6 ; :: thesis: verum

end;

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