let n be Nat; for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for b being Real ex g being PartFunc of REAL,REAL st
( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) )
let f be PartFunc of REAL,REAL; for Z being Subset of REAL
for b being Real ex g being PartFunc of REAL,REAL st
( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) )
let Z be Subset of REAL; for b being Real ex g being PartFunc of REAL,REAL st
( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) )
let b be Real; ex g being PartFunc of REAL,REAL st
( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) )
defpred S1[ set ] means $1 in Z;
deffunc H1( Real) -> Element of REAL = In (((f . b) - ((Partial_Sums (Taylor (f,Z,$1,b))) . n)),REAL);
consider g being PartFunc of REAL,REAL such that
A1:
for d being Element of REAL holds
( d in dom g iff S1[d] )
and
A2:
for d being Element of REAL st d in dom g holds
g /. d = H1(d)
from PARTFUN2:sch 2();
take
g
; ( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) )
for x being object st x in dom g holds
x in Z
by A1;
then A3:
dom g c= Z
by TARSKI:def 3;
for x being object st x in Z holds
x in dom g
by A1;
then A4:
Z c= dom g
by TARSKI:def 3;
for d being Real st d in Z holds
g . d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n)
proof
let d be
Real;
( d in Z implies g . d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n) )
assume A5:
d in Z
;
g . d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n)
g /. d =
H1(
d)
by A2, A4, A5
.=
(f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n)
;
hence
g . d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n)
by A4, A5, PARTFUN1:def 6;
verum
end;
hence
( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) )
by A3, A4, XBOOLE_0:def 10; verum