theorem Th25: :: MESFUN9C:25

for X being non empty set
for F being Functional_Sequence of X,COMPLEX holds
( Re F is with_the_same_dom iff Im F is with_the_same_dom )