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;

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

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