let n be Nat; :: thesis: 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) !))

let f be PartFunc of REAL,REAL; :: thesis: 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) !))

let Z be Subset of REAL; :: thesis: 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) !))

let b, l be Real; :: thesis: 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) !))

deffunc H_{1}( Real) -> Element of REAL = In ((((f . b) - ((Partial_Sums (Taylor (f,Z,$1,b))) . n)) - ((l * ((b - $1) |^ (n + 1))) / ((n + 1) !))),REAL);

consider g being Function of REAL,REAL such that

A1: for d being Element of REAL holds g . d = H_{1}(d)
from FUNCT_2:sch 4();

take g ; :: thesis: for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !))

let x be Real; :: thesis: g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !))

reconsider x = x as Element of REAL by XREAL_0:def 1;

g . x = H_{1}(x)
by A1;

hence g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ; :: thesis: verum

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) !))

let f be PartFunc of REAL,REAL; :: thesis: 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) !))

let Z be Subset of REAL; :: thesis: 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) !))

let b, l be Real; :: thesis: 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) !))

deffunc H

consider g being Function of REAL,REAL such that

A1: for d being Element of REAL holds g . d = H

take g ; :: thesis: for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !))

let x be Real; :: thesis: g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !))

reconsider x = x as Element of REAL by XREAL_0:def 1;

g . x = H

hence g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ; :: thesis: verum