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

( 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