reconsider zz = 0 , j = 1 as Element of REAL by XREAL_0:def 1;
<i> = [*zz,j*] by ARYTM_0:def 5, XCMPLX_0:def 1;
hence ( Re <i> = 0 & Im <i> = 1 ) by Lm2; :: thesis: verum