let X be non empty set ; :: thesis: for F being Functional_Sequence of X,REAL holds R_EAL F is additive
let F be Functional_Sequence of X,REAL; :: thesis: R_EAL F is additive

now :: thesis: for n, m being Nat st n <> m holds
for x being set holds
( not x in (dom ((R_EAL F) . n)) /\ (dom ((R_EAL F) . m)) or ((R_EAL F) . n) . x <> +infty or ((R_EAL F) . m) . x <> -infty )

let n, m be Nat; :: thesis: ( n <> m implies for x being set holds
( not x in (dom ((R_EAL F) . n)) /\ (dom ((R_EAL F) . m)) or ((R_EAL F) . n) . x <> +infty or ((R_EAL F) . m) . x <> -infty ) )
assume n <> m ; :: thesis: for x being set holds
( not x in (dom ((R_EAL F) . n)) /\ (dom ((R_EAL F) . m)) or ((R_EAL F) . n) . x <> +infty or ((R_EAL F) . m) . x <> -infty )
let x be set ; :: thesis: ( not x in (dom ((R_EAL F) . n)) /\ (dom ((R_EAL F) . m)) or ((R_EAL F) . n) . x <> +infty or ((R_EAL F) . m) . x <> -infty )
assume x in (dom ((R_EAL F) . n)) /\ (dom ((R_EAL F) . m)) ; :: thesis: ( ((R_EAL F) . n) . x <> +infty or ((R_EAL F) . m) . x <> -infty )
(R_EAL F) . n = R_EAL (F . n) ;
hence ( ((R_EAL F) . n) . x <> +infty or ((R_EAL F) . m) . x <> -infty ) ; :: thesis: verum

end;

hence R_EAL F is additive by MESFUNC9:def 5; :: thesis: verum