:: deftheorem Def4 defines #R TAYLOR_1:def 4 :
for p being Real
for b₂ being PartFunc of REAL,REAL holds
( b₂ = #R p iff ( dom b₂ = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b₂ . d = d #R p ) ) );