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 A1, Th15;
A3: dom (f `partial| (X,i)) = X by A2, PDIFF_9:def 6;

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 XREAL_0:def 1, FUNCT_2:5;
A7: partdiff (f,x1,i) = (diff (f,x1)) . ((reproj (i,(0* m))) . 1) by PDIFF_7:23, A5, A1
.= 0 by A6, FUNCOP_1:7, A5 ;
thus (f `partial| (X,i)) . x = (f `partial| (X,i)) /. x1 by A4, PARTFUN1:def 6
.= 0 by A7, A2, A4, A3, PDIFF_9:def 6 ; :: thesis: verum

end;

hence f `partial| (X,i) = X --> 0 by A3, FUNCOP_1:11; :: thesis: verum