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