let X be non empty set ; :: thesis: for F being Functional_Sequence of X,ExtREAL st F is with_the_same_dom holds

- F is with_the_same_dom

let F be Functional_Sequence of X,ExtREAL; :: thesis: ( F is with_the_same_dom implies - F is with_the_same_dom )

assume A1: F is with_the_same_dom ; :: thesis: - F is with_the_same_dom

- F is with_the_same_dom

let F be Functional_Sequence of X,ExtREAL; :: thesis: ( F is with_the_same_dom implies - F is with_the_same_dom )

assume A1: F is with_the_same_dom ; :: thesis: - F is with_the_same_dom

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

hence
- F is with_the_same_dom
by MESFUNC8:def 2; :: thesis: verumlet n, m be Nat; :: thesis: dom ((- F) . n) = dom ((- F) . m)

( (- F) . n = - (F . n) & (- F) . m = - (F . m) ) by Th37;

then ( dom ((- F) . n) = dom (F . n) & dom ((- F) . m) = dom (F . m) ) by MESFUNC1:def 7;

hence dom ((- F) . n) = dom ((- F) . m) by A1, MESFUNC8:def 2; :: thesis: verum

end;( (- F) . n = - (F . n) & (- F) . m = - (F . m) ) by Th37;

then ( dom ((- F) . n) = dom (F . n) & dom ((- F) . m) = dom (F . m) ) by MESFUNC1:def 7;

hence dom ((- F) . n) = dom ((- F) . m) by A1, MESFUNC8:def 2; :: thesis: verum