let m be non zero Element of NAT ; :: thesis: for Z being set
for i being Nat
for f being PartFunc of (REAL m),REAL holds
( f is_partial_differentiable_on Z,i iff f | Z is_partial_differentiable_on Z,i )
let Z be set ; :: thesis: for i being Nat
for f being PartFunc of (REAL m),REAL holds
( f is_partial_differentiable_on Z,i iff f | Z is_partial_differentiable_on Z,i )
let i be Nat; :: thesis: for f being PartFunc of (REAL m),REAL holds
( f is_partial_differentiable_on Z,i iff f | Z is_partial_differentiable_on Z,i )
let f be PartFunc of (REAL m),REAL; :: thesis: ( f is_partial_differentiable_on Z,i iff f | Z is_partial_differentiable_on Z,i )

hereby :: thesis: ( f | Z is_partial_differentiable_on Z,i implies f is_partial_differentiable_on Z,i )

assume A1: f is_partial_differentiable_on Z,i ; :: thesis: f | Z is_partial_differentiable_on Z,i
(f | Z) | Z = f | Z by RELAT_1:72;
hence f | Z is_partial_differentiable_on Z,i by A1, RELAT_1:62; :: thesis: verum

end;

assume A2: f | Z is_partial_differentiable_on Z,i ; :: thesis: f is_partial_differentiable_on Z,i
dom (f | Z) c= dom f by RELAT_1:60;
then A3: Z c= dom f by A2;
(f | Z) | Z = f | Z by RELAT_1:72;
hence f is_partial_differentiable_on Z,i by A2, A3; :: thesis: verum