theorem Th18: :: MESFUNC9:18

for X being non empty set
for F, G being Functional_Sequence of X,ExtREAL
for D being set st F is with_the_same_dom & ( for n being Nat holds G . n = (F . n) | D ) holds
G is with_the_same_dom