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