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

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 = - (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;

hence - F is with_the_same_dom by MESFUNC8:def 2; :: thesis: verum