let X be non empty set ; :: thesis: 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
let F be FinSequence of Funcs (X,ExtREAL); :: thesis: ( ( F is without_+infty-valued or F is without_-infty-valued ) implies for n, m being Nat st n in dom F & m in dom F holds
dom ((F /. n) + (F /. m)) = X )
assume A1: ( F is without_+infty-valued or F is without_-infty-valued ) ; :: thesis: for n, m being Nat st n in dom F & m in dom F holds
dom ((F /. n) + (F /. m)) = X

per cases ( F is without_+infty-valued or F is without_-infty-valued ) by A1;

suppose A2: F is without_+infty-valued ; :: thesis: for n, m being Nat st n in dom F & m in dom F holds
dom ((F /. n) + (F /. m)) = X

let n, m be Nat; :: thesis: ( n in dom F & m in dom F implies dom ((F /. n) + (F /. m)) = X )
assume ( n in dom F & m in dom F ) ; :: thesis: dom ((F /. n) + (F /. m)) = X
then ( (F /. n) " {+infty} = {} & (F /. m) " {+infty} = {} ) by A2, Th53;
then A4: ((dom (F /. n)) /\ (dom (F /. m))) \ ((((F /. n) " {-infty}) /\ ((F /. m) " {+infty})) \/ (((F /. n) " {+infty}) /\ ((F /. m) " {-infty}))) = (dom (F /. n)) /\ (dom (F /. m)) ;
( dom (F /. n) = X & dom (F /. m) = X ) by FUNCT_2:def 1;
hence dom ((F /. n) + (F /. m)) = X by A4, MESFUNC1:def 3; :: thesis: verum

end;

suppose A5: F is without_-infty-valued ; :: thesis: for n, m being Nat st n in dom F & m in dom F holds
dom ((F /. n) + (F /. m)) = X

let n, m be Nat; :: thesis: ( n in dom F & m in dom F implies dom ((F /. n) + (F /. m)) = X )
assume ( n in dom F & m in dom F ) ; :: thesis: dom ((F /. n) + (F /. m)) = X
then ( (F /. n) " {-infty} = {} & (F /. m) " {-infty} = {} ) by A5, Th54;
then A7: ((dom (F /. n)) /\ (dom (F /. m))) \ ((((F /. n) " {-infty}) /\ ((F /. m) " {+infty})) \/ (((F /. n) " {+infty}) /\ ((F /. m) " {-infty}))) = (dom (F /. n)) /\ (dom (F /. m)) ;
( dom (F /. n) = X & dom (F /. m) = X ) by FUNCT_2:def 1;
hence dom ((F /. n) + (F /. m)) = X by A7, MESFUNC1:def 3; :: thesis: verum

end;

end;