deffunc H₁( Nat) -> Element of bool [:X,ExtREAL:] = <:{},X,ExtREAL:>;
consider F being Functional_Sequence of X,ExtREAL such that
A1: for n being Nat holds F . n = H₁(n) from SEQFUNC:sch 1();

now :: thesis: for n, m being Nat holds dom (F . n) = dom (F . m)

let n, m be Nat; :: thesis: dom (F . n) = dom (F . m)
F . n = <:{},X,ExtREAL:> by A1;
hence dom (F . n) = dom (F . m) by A1; :: thesis: verum

end;

then reconsider F = F as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
take F ; :: thesis: ( F is additive & F is with_the_same_dom )

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 A2: x in (dom (F . n)) /\ (dom (F . m)) ; :: thesis: ( (F . n) . x <> +infty or (F . m) . x <> -infty )
F . n = <:{},X,ExtREAL:> by A1;
then x in (dom {}) /\ (dom (F . m)) by A2, PARTFUN1:34;
hence ( (F . n) . x <> +infty or (F . m) . x <> -infty ) ; :: thesis: verum

end;

hence ( F is additive & F is with_the_same_dom ) ; :: thesis: verum