let m be non zero Element of NAT ; 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 ; 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; 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; ( f is_partial_differentiable_on Z,i iff f | Z is_partial_differentiable_on Z,i )
assume A2:
f | Z is_partial_differentiable_on Z,i
; 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; verum