let n be Nat; :: thesis:
let f be PartFunc of REAL,REAL; :: thesis:
let Z be Subset of REAL; :: thesis:
let b be Real; :: thesis:
defpred S₁[ set ] means $1 in Z;
deffunc H₁( 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₁[d] ) and
A2: for d being Element of REAL st d in dom g holds
g /. d = H₁(d) from PARTFUN2:sch 2();
take g ; :: thesis:
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)

let d be Real; :: thesis:
assume A5: d in Z ; :: thesis:
g /. d = H₁(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:

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