let X be non empty set ; :: thesis: for F being Functional_Sequence of X,ExtREAL st F is additive holds
- F is additive
let F be Functional_Sequence of X,ExtREAL; :: thesis: ( F is additive implies - F is additive )
assume A1: F is additive ; :: thesis: - F is additive

now :: thesis: 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 )

let n, m be Nat; :: 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 )
let x be set ; :: thesis: ( not x in (dom ((- F) . n)) /\ (dom ((- F) . m)) or ((- F) . n) . x <> +infty or ((- F) . m) . x <> -infty )
assume x in (dom ((- F) . n)) /\ (dom ((- F) . m)) ; :: thesis: ( ((- F) . n) . x <> +infty or ((- F) . m) . x <> -infty )
then x in (dom (- (F . n))) /\ (dom ((- F) . m)) by Th37;
then A3: x in (dom (- (F . n))) /\ (dom (- (F . m))) by Th37;
then ( x in dom (- (F . n)) & x in dom (- (F . m)) ) by XBOOLE_0:def 4;
then ( (- (F . n)) . x = - ((F . n) . x) & (- (F . m)) . x = - ((F . m) . x) ) by MESFUNC1:def 7;
then A4: ( ((- F) . n) . x = - ((F . n) . x) & ((- F) . m) . x = - ((F . m) . x) ) by Th37;
x in (dom (F . n)) /\ (dom (- (F . m))) by A3, MESFUNC1:def 7;
then x in (dom (F . n)) /\ (dom (F . m)) by MESFUNC1:def 7;
hence ( ((- F) . n) . x <> +infty or ((- F) . m) . x <> -infty ) by A4, XXREAL_3:6, A1, MESFUNC9:def 5; :: thesis: verum

end;

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