theorem :: INTEGR16:12

for A being non empty Subset of REAL
for f being PartFunc of REAL,COMPLEX
for g being Function of A,COMPLEX st f = g holds
( Re f = Re g & Im f = Im g ) ;