for X being non empty set
for F being FinSequence of Funcs (X,ExtREAL) st ( F is without_+infty-valued or F is without_-infty-valued ) holds
for n, m being Nat st n in dom F & m in dom F holds
dom ((F /. n) + (F /. m)) = X