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

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;

+ (Z,Z) = 0 by ARYTM_0:11;

then Lm2: opp Z = 0 by ARYTM_0:def 3;

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

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

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

.= [*(+ ((* (x1,Z)),(opp Z))),(+ ((* (x1,Z)),Z))*] by ARYTM_0:12

.= [*(+ (Z,(opp Z))),(+ ((* (x1,Z)),Z))*] by ARYTM_0:12

.= [*(+ (Z,(opp Z))),(+ (Z,Z))*] by ARYTM_0:12

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

.= [*(opp Z),Z*] by ARYTM_0:11

.= 0 by Lm2, ARYTM_0:def 5 ;

hence x * 0 = 0 ; :: 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;

+ (Z,Z) = 0 by ARYTM_0:11;

then Lm2: opp Z = 0 by ARYTM_0:def 3;

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

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

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

.= [*(+ ((* (x1,Z)),(opp Z))),(+ ((* (x1,Z)),Z))*] by ARYTM_0:12

.= [*(+ (Z,(opp Z))),(+ ((* (x1,Z)),Z))*] by ARYTM_0:12

.= [*(+ (Z,(opp Z))),(+ (Z,Z))*] by ARYTM_0:12

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

.= [*(opp Z),Z*] by ARYTM_0:11

.= 0 by Lm2, ARYTM_0:def 5 ;

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