:: deftheorem defines <i> XCMPLX_0:def 1 :
<i> = (0,1) --> (0,1);