let X be non empty set ; :: thesis: for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is nonnegative ) holds
F is additive
let F be Functional_Sequence of X,ExtREAL; :: thesis: ( ( for n being Nat holds F . n is nonnegative ) implies F is additive )
assume A1: for n being Nat holds F . n is nonnegative ; :: thesis: F is additive
let n, m be Nat; :: according to MESFUNC9:def 5 :: thesis: ( n <> m implies for x being set holds
( not x in (dom (F . n)) /\ (dom (F . m)) or (F . n) . x <> +infty or (F . m) . x <> -infty ) )
assume n <> m ; :: thesis: for x being set holds
( not x in (dom (F . n)) /\ (dom (F . m)) or (F . n) . x <> +infty or (F . m) . x <> -infty )
F . m is nonnegative by A1;
hence 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 SUPINF_2:51; :: thesis: verum