theorem :: XCMPLX_1:15

for a, b being Complex st a - b = 0 holds
a = b ;