theorem Th20: :: MESFUN9C:20

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