theorem Th23: :: MESFUN7C:23

for X being non empty set
for f being with_the_same_dom Functional_Sequence of X,COMPLEX
for x being Element of X st x in dom (f . 0) holds
( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) )