theorem :: COMPLSP2:44

for x1, y1 being Element of COMPLEX
for x2, y2 being Real st x1 = x2 & y1 = y2 holds
addcomplex . (x1,y1) = addreal . (x2,y2)