let X be non empty set ; :: thesis: for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is without-infty ) holds
F is additive
let F be Functional_Sequence of X,ExtREAL; :: thesis: ( ( for n being Nat holds F . n is without-infty ) implies F is additive )
assume for n being Nat holds F . n is without-infty ; :: thesis: F is additive
then for n, m being Nat st n <> m holds
for x being set holds
( not x in (dom (F . n)) /\ (dom (F . m)) or (F . n) . x <> +infty or (F . m) . x <> -infty ) by MESFUNC5:def 5;
hence F is additive by MESFUNC9:def 5; :: thesis: verum