let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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 S_{1}[ set ] means $1 in Z;

deffunc H_{1}( 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 S_{1}[d] )
and

A2: for d being Element of REAL st d in dom g holds

g /. d = H_{1}(d)
from PARTFUN2:sch 2();

take g ; :: thesis: ( 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)

g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) ) by A3, A4, XBOOLE_0:def 10; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: 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 S

deffunc H

consider g being PartFunc of REAL,REAL such that

A1: for d being Element of REAL holds

( d in dom g iff S

A2: for d being Element of REAL st d in dom g holds

g /. d = H

take g ; :: thesis: ( 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

hence
( dom g = Z & ( for x being Real st x in Z holds
let d be Real; :: thesis: ( d in Z implies g . d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n) )

assume A5: d in Z ; :: thesis: g . d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n)

g /. d = H_{1}(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; :: thesis: verum

end;assume A5: d in Z ; :: thesis: g . d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n)

g /. d = H

.= (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; :: thesis: verum

g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) ) by A3, A4, XBOOLE_0:def 10; :: thesis: verum