let n be Element of 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₁( Real) -> Element of REAL = ((f . b) - ((Partial_Sums (Taylor f,Z,$1,b)) . n)) - ((l * ((b - $1) |^ (n + 1))) / ((n + 1) ! ));
consider g being Function of REAL ,REAL such that
A1: for d being Element of REAL holds g . d = H₁(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) ! ))
thus for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor f,Z,x,b)) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) ! )) by A1; :: thesis: verum