:: deftheorem defines additive MESFUNC9:def 5 :
for X being set
for F being Functional_Sequence of X,ExtREAL holds
( F is additive iff 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 ) );