let x be Complex; :: thesis: 1 * x = x
( 0 in NAT & 1 in NAT ) ;
then reconsider Z = 0 , J = 1 as Element of REAL by NUMBERS:19;
+ (Z,Z) = 0 by ARYTM_0:11;
then Lm2: opp Z = 0 by ARYTM_0:def 3;
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 = [*J,Z*] by ARYTM_0:def 5;
then x * 1 = [*(+ ((* (x1,J)),(opp (* (x2,Z))))),(+ ((* (x1,Z)),(* (x2,J))))*] by A1, XCMPLX_0:def 5
.= [*(+ ((* (x1,J)),(opp Z))),(+ ((* (x1,Z)),(* (x2,J))))*] by ARYTM_0:12
.= [*(+ (x1,(opp Z))),(+ ((* (x1,Z)),(* (x2,J))))*] by ARYTM_0:19
.= [*(+ (x1,(opp Z))),(+ ((* (x1,Z)),x2))*] by ARYTM_0:19
.= [*(+ (x1,Z)),(+ (Z,x2))*] by Lm2, ARYTM_0:12
.= [*x1,(+ (Z,x2))*] by ARYTM_0:11
.= x by A1, ARYTM_0:11 ;
hence 1 * x = x ; :: thesis: verum