let X be non empty set ; :: thesis: for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is V120() ) holds

F is additive

let F be Functional_Sequence of X,ExtREAL; :: thesis: ( ( for n being Nat holds F . n is V120() ) implies F is additive )

assume for n being Nat holds F . n is V120() ; :: 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

F is additive

let F be Functional_Sequence of X,ExtREAL; :: thesis: ( ( for n being Nat holds F . n is V120() ) implies F is additive )

assume for n being Nat holds F . n is V120() ; :: 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