for n being Nat
for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for b, l being Real ex g being Function of REAL,REAL st
for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !))