let x be complex number ; :: thesis: 1 * x = 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;
1 = [*1,0 *] by ARYTM_0:def 7;
then x * 1 = [*(+ (* x1,1),(opp (* x2,0 ))),(+ (* x1,0 ),(* x2,1))*] by A1, XCMPLX_0:def 5
.= [*(+ (* x1,1),(opp 0 )),(+ (* x1,0 ),(* x2,1))*] by ARYTM_0:14
.= [*(+ x1,(opp 0 )),(+ (* x1,0 ),(* x2,1))*] by ARYTM_0:21
.= [*(+ x1,(opp 0 )),(+ (* x1,0 ),x2)*] by ARYTM_0:21
.= [*(+ x1,0 ),(+ 0 ,x2)*] by Lm2, ARYTM_0:14
.= [*x1,(+ 0 ,x2)*] by ARYTM_0:13
.= x by A1, ARYTM_0:13 ;
hence 1 * x = x ; :: thesis: verum