let x be Complex; :: thesis: x + 0 = x

0 in NAT ;

then reconsider Z = 0 as Element of REAL by NUMBERS:19;

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:9;

0 = [*Z,Z*] by ARYTM_0:def 5;

then x + 0 = [*(+ (x1,Z)),(+ (x2,Z))*] by A1, XCMPLX_0:def 4

.= [*x1,(+ (x2,Z))*] by ARYTM_0:11

.= x by A1, ARYTM_0:11 ;

hence x + 0 = x ; :: thesis: verum

0 in NAT ;

then reconsider Z = 0 as Element of REAL by NUMBERS:19;

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:9;

0 = [*Z,Z*] by ARYTM_0:def 5;

then x + 0 = [*(+ (x1,Z)),(+ (x2,Z))*] by A1, XCMPLX_0:def 4

.= [*x1,(+ (x2,Z))*] by ARYTM_0:11

.= x by A1, ARYTM_0:11 ;

hence x + 0 = x ; :: thesis: verum