let X be non empty set ; :: thesis: for F being Functional_Sequence of X,COMPLEX holds

( Re F is with_the_same_dom iff Im F is with_the_same_dom )

let F be Functional_Sequence of X,COMPLEX; :: thesis: ( Re F is with_the_same_dom iff Im F is with_the_same_dom )

hence Re F is with_the_same_dom ; :: thesis: verum

( Re F is with_the_same_dom iff Im F is with_the_same_dom )

let F be Functional_Sequence of X,COMPLEX; :: thesis: ( Re F is with_the_same_dom iff Im F is with_the_same_dom )

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

assume A1:
Im F is with_the_same_dom
; :: thesis: Re F is with_the_same_dom assume
Re F is with_the_same_dom
; :: thesis: Im F is with_the_same_dom

then F is with_the_same_dom by Th24;

then for n, m being Nat holds dom ((Im F) . n) = dom ((Im F) . m) by MESFUN7C:def 12, MESFUNC8:def 2;

hence Im F is with_the_same_dom ; :: thesis: verum

end;then F is with_the_same_dom by Th24;

then for n, m being Nat holds dom ((Im F) . n) = dom ((Im F) . m) by MESFUN7C:def 12, MESFUNC8:def 2;

hence Im F is with_the_same_dom ; :: thesis: verum

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

then
F is with_the_same_dom
;let n, m be Nat; :: thesis: dom (F . n) = dom (F . m)

( dom ((Im F) . n) = dom (F . n) & dom ((Im F) . m) = dom (F . m) ) by MESFUN7C:def 12;

hence dom (F . n) = dom (F . m) by A1; :: thesis: verum

end;( dom ((Im F) . n) = dom (F . n) & dom ((Im F) . m) = dom (F . m) ) by MESFUN7C:def 12;

hence dom (F . n) = dom (F . m) by A1; :: thesis: verum

hence Re F is with_the_same_dom ; :: thesis: verum