let x be complex number ; :: thesis: x + 0 = x
x in COMPLEX by XCMPLX_0:def 2;
then consider x1, x2 being Element of REAL such that
A1: x = [*x1,x2*] by ARYTM_0:11;
0 = [*0 ,0 *] by ARYTM_0:def 7;
then x + 0 = [*(+ x1,0 ),(+ x2,0 )*] by A1, XCMPLX_0:def 4
.= [*x1,(+ x2,0 )*] by ARYTM_0:13
.= x by A1, ARYTM_0:13 ;
hence x + 0 = x ; :: thesis: verum