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