theorem Th45: :: PDIFF_7:45

for m being non zero Nat
for f being PartFunc of (REAL m),REAL
for X being Subset of (REAL m)
for x, y, z being Element of REAL m
for i being Nat
for d, p, q being Real st 1 <= i & i <= m & X is open & x in X & |.(y - x).| < d & |.(z - x).| < d & X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,i ) & 0 < d & ( for z being Element of REAL m st |.(z - x).| < d holds
z in X ) & z = (reproj (i,y)) . p & q = (proj (i,m)) . y holds
ex w being Element of REAL m st
( |.(w - x).| < d & f is_partial_differentiable_in w,i & (f /. z) - (f /. y) = (p - q) * (partdiff (f,w,i)) )