theorem Th28: :: PDIFF_7:28

for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for x, y being Element of REAL m ex h being FinSequence of REAL m ex g being FinSequence of REAL n st
( len h = m + 1 & len g = m & ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) & ( for i being Nat st i in dom g holds
g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))) ) & ( for i being Nat
for hi being Element of REAL m st i in dom h & h /. i = hi holds
|.hi.| <= |.y.| ) & (f /. (x + y)) - (f /. x) = Sum g )