theorem Th27: :: MESFUNC8:27

for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL st ( for x being Element of X st x in dom g holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds
g is real-valued