let m be non zero Element of NAT ; 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); 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; 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; ( 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 )
; 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;
( x in Z implies (f `partial| (Z,i)) /. x = partdiff ((f | Z),x,i) )
assume A3:
x in Z
;
(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;
verum
end;
hence
f `partial| (Z,i) = (f | Z) `partial| (Z,i)
by A1, A2, Def6; verum