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:9;
1 = [*1,0*] by ARYTM_0:def 5;
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:12
.= [*(+ (x1,(opp 0))),(+ ((* (x1,0)),(* (x2,1))))*] by ARYTM_0:19
.= [*(+ (x1,(opp 0))),(+ ((* (x1,0)),x2))*] by ARYTM_0:19
.= [*(+ (x1,0)),(+ (0,x2))*] by Lm2, ARYTM_0:12
.= [*x1,(+ (0,x2))*] by ARYTM_0:11
.= x by A1, ARYTM_0:11 ;
hence 1 * x = x ; :: thesis: verum