let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T
for Z being Subset of S holds
( f | Z is_differentiable_on Z iff f is_differentiable_on Z )
let f be PartFunc of S,T; :: thesis: for Z being Subset of S holds
( f | Z is_differentiable_on Z iff f is_differentiable_on Z )
let Z be Subset of S; :: thesis: ( f | Z is_differentiable_on Z iff f is_differentiable_on Z )

hereby :: thesis: ( f is_differentiable_on Z implies f | Z is_differentiable_on Z )

assume A1: f | Z is_differentiable_on Z ; :: thesis: f is_differentiable_on Z
dom (f | Z) c= dom f by RELAT_1:60;
hence f is_differentiable_on Z by A1, XBOOLE_1:1; :: thesis: verum

end;

thus ( f is_differentiable_on Z implies f | Z is_differentiable_on Z ) by RELAT_1:62; :: thesis: verum