theorem Th12: :: MESFUNC9:12

for X being non empty set
for F, G being Functional_Sequence of X,ExtREAL
for x being Element of X
for D being set st ( for n being Nat holds G . n = (F . n) | D ) & x in D holds
( ( F # x is convergent_to_+infty implies G # x is convergent_to_+infty ) & ( F # x is convergent_to_-infty implies G # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies G # x is convergent_to_finite_number ) & ( F # x is convergent implies G # x is convergent ) )