let X be non empty set ; :: thesis: for F being Functional_Sequence of X,COMPLEX holds
( F is with_the_same_dom iff Re F is with_the_same_dom )
let F be Functional_Sequence of X,COMPLEX ; :: thesis: ( F is with_the_same_dom iff Re F is with_the_same_dom )

hereby :: thesis: ( Re F is with_the_same_dom implies F is with_the_same_dom )

assume A0: F is with_the_same_dom ; :: thesis: Re F is with_the_same_dom

now

let n, m be natural number ; :: thesis: dom ((Re F) . n) = dom ((Re F) . m)
( dom ((Re F) . n) = dom (F . n) & dom ((Re F) . m) = dom (F . m) ) by MESFUN7C:def 11;
hence dom ((Re F) . n) = dom ((Re F) . m) by A0, MESFUNC8:def 2; :: thesis: verum

end;

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

end;

assume B0: Re F is with_the_same_dom ; :: thesis: F is with_the_same_dom

now

let n, m be natural number ; :: thesis: dom (F . n) = dom (F . m)
( dom ((Re F) . n) = dom (F . n) & dom ((Re F) . m) = dom (F . m) ) by MESFUN7C:def 11;
hence dom (F . n) = dom (F . m) by B0, MESFUNC8:def 2; :: thesis: verum

end;

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