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