y in COMPLEX by XCMPLX_0:def 2;
hence the carrier of X --> y is Function of the carrier of X,COMPLEX by FUNCOP_1:45; :: thesis: verum