theorem :: MESFUN15:54

for f being PartFunc of REAL,REAL
for a, b being Real st [.a,b.[ = dom f holds
ex F being Functional_Sequence of REAL,REAL st
( ( for n being Nat holds
( dom (F . n) = dom f & ( for x being Real st x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = f . x ) & ( for x being Real st not x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = 0 ) ) ) & lim (R_EAL F) = f )