theorem Th7: :: MESFUN6C:7

for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A being Element of S holds
( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )