let m be non zero Element of NAT ; :: thesis: for i being Element of NAT
for f being PartFunc of (REAL m),REAL
for X being non empty Subset of (REAL m)
for d being Real st X is open & f = X --> d & 1 <= i & i <= m holds
f `partial| (X,i) = X --> 0

let i be Element of NAT ; :: thesis: for f being PartFunc of (REAL m),REAL
for X being non empty Subset of (REAL m)
for d being Real st X is open & f = X --> d & 1 <= i & i <= m holds
f `partial| (X,i) = X --> 0

let f be PartFunc of (REAL m),REAL; :: thesis: for X being non empty Subset of (REAL m)
for d being Real st X is open & f = X --> d & 1 <= i & i <= m holds
f `partial| (X,i) = X --> 0

let X be non empty Subset of (REAL m); :: thesis: for d being Real st X is open & f = X --> d & 1 <= i & i <= m holds
f `partial| (X,i) = X --> 0

let d be Real; :: thesis: ( X is open & f = X --> d & 1 <= i & i <= m implies f `partial| (X,i) = X --> 0 )
assume A1: ( X is open & f = X --> d & 1 <= i & i <= m ) ; :: thesis: f `partial| (X,i) = X --> 0
A2: f is_partial_differentiable_on X,i by ;
A3: dom (f `partial| (X,i)) = X by ;
now :: thesis: for x being object st x in dom (f `partial| (X,i)) holds
(f `partial| (X,i)) . x = 0
let x be object ; :: thesis: ( x in dom (f `partial| (X,i)) implies (f `partial| (X,i)) . x = 0 )
assume A4: x in dom (f `partial| (X,i)) ; :: thesis: (f `partial| (X,i)) . x = 0
then reconsider x1 = x as Element of REAL m ;
A5: ( f is_differentiable_in x1 & diff (f,x1) = (REAL m) --> 0 ) by Th12, A1, A3, A4;
A6: (reproj (i,(0* m))) . 1 in REAL m by ;
A7: partdiff (f,x1,i) = (diff (f,x1)) . ((reproj (i,(0* m))) . 1) by
.= 0 by ;
thus (f `partial| (X,i)) . x = (f `partial| (X,i)) /. x1 by
.= 0 by ; :: thesis: verum
end;
hence f `partial| (X,i) = X --> 0 by ; :: thesis: verum