let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T
for Z being Subset of S
for x being Point of S st Z is open & x in Z & Z c= dom f holds
( f | Z is_differentiable_in x iff f is_differentiable_in x )
let f be PartFunc of S,T; :: thesis: for Z being Subset of S
for x being Point of S st Z is open & x in Z & Z c= dom f holds
( f | Z is_differentiable_in x iff f is_differentiable_in x )
let Z be Subset of S; :: thesis: for x being Point of S st Z is open & x in Z & Z c= dom f holds
( f | Z is_differentiable_in x iff f is_differentiable_in x )
let x0 be Point of S; :: thesis: ( Z is open & x0 in Z & Z c= dom f implies ( f | Z is_differentiable_in x0 iff f is_differentiable_in x0 ) )
assume A1: ( Z is open & x0 in Z & Z c= dom f ) ; :: thesis: ( f | Z is_differentiable_in x0 iff f is_differentiable_in x0 )

hereby :: thesis: ( f is_differentiable_in x0 implies f | Z is_differentiable_in x0 )

assume A2: f | Z is_differentiable_in x0 ; :: thesis: f is_differentiable_in x0
thus f is_differentiable_in x0 :: thesis: verum

proof

consider N being Neighbourhood of x0 such that
A3: N c= dom (f | Z) and
A4: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A2;
consider L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R being RestFunc of S,T such that
A5: for x being Point of S st x in N holds
((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A4;
take N ; :: according to NDIFF_1:def 6 :: thesis: ( N c= dom f & ex b₁ being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex b₂ being Element of bool [: the carrier of S, the carrier of T:] st
for b₃ being Element of the carrier of S holds
( not b₃ in N or (f /. b₃) - (f /. x0) = (b₁ . (b₃ - x0)) + (b₂ /. (b₃ - x0)) ) )
A6: dom (f | Z) = (dom f) /\ Z by RELAT_1:61;
then dom (f | Z) c= dom f by XBOOLE_1:17;
hence N c= dom f by A3, XBOOLE_1:1; :: thesis: ex b₁ being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex b₂ being Element of bool [: the carrier of S, the carrier of T:] st
for b₃ being Element of the carrier of S holds
( not b₃ in N or (f /. b₃) - (f /. x0) = (b₁ . (b₃ - x0)) + (b₂ /. (b₃ - x0)) )
take L ; :: thesis: ex b₁ being Element of bool [: the carrier of S, the carrier of T:] st
for b₂ being Element of the carrier of S holds
( not b₂ in N or (f /. b₂) - (f /. x0) = (L . (b₂ - x0)) + (b₁ /. (b₂ - x0)) )
take R ; :: thesis: for b₁ being Element of the carrier of S holds
( not b₁ in N or (f /. b₁) - (f /. x0) = (L . (b₁ - x0)) + (R /. (b₁ - x0)) )
let x be Point of S; :: thesis: ( not x in N or (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
assume A7: x in N ; :: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then ((f | Z) /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A5;
then (f /. x) - ((f | Z) /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A3, A6, A7, PARTFUN2:16;
hence (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1, PARTFUN2:17; :: thesis: verum

end;

end;

thus ( f is_differentiable_in x0 implies f | Z is_differentiable_in x0 ) by A1, NDIFF_9:1; :: thesis: verum