let n be Element of NAT ; :: thesis: for f being PartFunc of REAL ,REAL
for x0, r being Real st 0 < r & ].(x0 - r),(x0 + r).[ c= dom f & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ holds
for x being Real st x in ].(x0 - r),(x0 + r).[ holds
ex s being Real st
( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Taylor f,].(x0 - r),(x0 + r).[,x0,x)) . n)) = abs (((((diff f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) ! )) )
let f be PartFunc of REAL ,REAL ; :: thesis: for x0, r being Real st 0 < r & ].(x0 - r),(x0 + r).[ c= dom f & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ holds
for x being Real st x in ].(x0 - r),(x0 + r).[ holds
ex s being Real st
( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Taylor f,].(x0 - r),(x0 + r).[,x0,x)) . n)) = abs (((((diff f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) ! )) )
let x0, r be Real; :: thesis: ( 0 < r & ].(x0 - r),(x0 + r).[ c= dom f & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ implies for x being Real st x in ].(x0 - r),(x0 + r).[ holds
ex s being Real st
( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Taylor f,].(x0 - r),(x0 + r).[,x0,x)) . n)) = abs (((((diff f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) ! )) ) )
assume that
A1: 0 < r and
A0: ].(x0 - r),(x0 + r).[ c= dom f and
A2: f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ ; :: thesis: for x being Real st x in ].(x0 - r),(x0 + r).[ holds
ex s being Real st
( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Taylor f,].(x0 - r),(x0 + r).[,x0,x)) . n)) = abs (((((diff f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) ! )) )
let x be Real; :: thesis: ( x in ].(x0 - r),(x0 + r).[ implies ex s being Real st
( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Taylor f,].(x0 - r),(x0 + r).[,x0,x)) . n)) = abs (((((diff f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) ! )) ) )
assume A3: x in ].(x0 - r),(x0 + r).[ ; :: thesis: ex s being Real st
( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Taylor f,].(x0 - r),(x0 + r).[,x0,x)) . n)) = abs (((((diff f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) ! )) )
consider s being Real such that
A4: ( 0 < s & s < 1 ) and
A5: f . x = ((Partial_Sums (Taylor f,].(x0 - r),(x0 + r).[,x0,x)) . n) + (((((diff f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) ! )) by A1, A2, A3, A0, TAYLOR_1:33;
thus ex s being Real st
( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Taylor f,].(x0 - r),(x0 + r).[,x0,x)) . n)) = abs (((((diff f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) ! )) ) by A4, A5; :: thesis: verum