let m be non zero Element of NAT ; :: thesis: for Z being Subset of (REAL m)
for i being Nat
for f being PartFunc of (REAL m),REAL st Z is open & 1 <= i & i <= m & f is_partial_differentiable_on Z,i holds
f `partial| (Z,i) = (f | Z) `partial| (Z,i)
let Z be Subset of (REAL m); :: thesis: for i being Nat
for f being PartFunc of (REAL m),REAL st Z is open & 1 <= i & i <= m & f is_partial_differentiable_on Z,i holds
f `partial| (Z,i) = (f | Z) `partial| (Z,i)
let i be Nat; :: thesis: for f being PartFunc of (REAL m),REAL st Z is open & 1 <= i & i <= m & f is_partial_differentiable_on Z,i holds
f `partial| (Z,i) = (f | Z) `partial| (Z,i)
let f be PartFunc of (REAL m),REAL; :: thesis: ( Z is open & 1 <= i & i <= m & f is_partial_differentiable_on Z,i implies f `partial| (Z,i) = (f | Z) `partial| (Z,i) )
assume A1: ( Z is open & 1 <= i & i <= m & f is_partial_differentiable_on Z,i ) ; :: thesis: f `partial| (Z,i) = (f | Z) `partial| (Z,i)
then A2: dom (f `partial| (Z,i)) = Z by Def6;
for x being Element of REAL m st x in Z holds
(f `partial| (Z,i)) /. x = partdiff ((f | Z),x,i)

proof

let x be Element of REAL m; :: thesis: ( x in Z implies (f `partial| (Z,i)) /. x = partdiff ((f | Z),x,i) )
assume A3: x in Z ; :: thesis: (f `partial| (Z,i)) /. x = partdiff ((f | Z),x,i)
then ( f is_partial_differentiable_in x,i & (f `partial| (Z,i)) /. x = partdiff (f,x,i) ) by A1, Def6, Th60;
hence (f `partial| (Z,i)) /. x = partdiff ((f | Z),x,i) by A1, A3, Th69; :: thesis: verum

end;

hence f `partial| (Z,i) = (f | Z) `partial| (Z,i) by A1, A2, Def6; :: thesis: verum