z in COMPLEX by XCMPLX_0:def 2;
then [z,z] in [:COMPLEX,COMPLEX:] by ZFMISC_1:87;
then [z,z] in dom addcomplex by FUNCT_2:def 1;
then z in dom (curry addcomplex) by FUNCT_5:19;
hence ( (curry addcomplex) . z is Function-like & (curry addcomplex) . z is Relation-like ) by FUNCT_5:30; :: thesis: verum