let X be non empty set ; :: thesis: 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
let f be Functional_Sequence of X,ExtREAL; :: thesis: 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
let g be PartFunc of X,ExtREAL; :: thesis: ( ( for x being Element of X st x in dom g holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) implies g is real-valued )
assume A1: for x being Element of X st x in dom g holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ; :: thesis: g is real-valued

now :: thesis: for x being Element of X st x in dom g holds
|.(g . x).| < +infty

let x be Element of X; :: thesis: ( x in dom g implies |.(g . x).| < +infty )
assume A2: x in dom g ; :: thesis: |.(g . x).| < +infty
then A3: ( not lim (f # x) = +infty or not f # x is convergent_to_+infty ) by A1, MESFUNC5:50;
f # x is convergent_to_finite_number by A1, A2;
then A4: f # x is convergent by MESFUNC5:def 11;
( not lim (f # x) = -infty or not f # x is convergent_to_-infty ) by A1, A2, MESFUNC5:51;
then consider g0 being Real such that
A5: lim (f # x) = g0 and
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((f # x) . m) - (lim (f # x))).| < p and
f # x is convergent_to_finite_number by A4, A3, MESFUNC5:def 12;
|.(g . x).| = |.g0.| by A1, A2, A5, EXTREAL1:12;
hence |.(g . x).| < +infty by XXREAL_0:9, XREAL_0:def 1; :: thesis: verum

end;

hence g is real-valued by MESFUNC2:def 1; :: thesis: verum