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