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:11;
0 = [*0 ,0 *] by ARYTM_0:def 7;
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:14
.= [*(+ (* x1,0 ),(opp 0 )),(+ (* x1,0 ),0 )*] by ARYTM_0:14
.= [*(+ 0 ,(opp 0 )),(+ (* x1,0 ),0 )*] by ARYTM_0:14
.= [*(+ 0 ,(opp 0 )),(+ 0 ,0 )*] by ARYTM_0:14
.= [*(+ 0 ,(opp 0 )),0 *] by ARYTM_0:13
.= [*(opp 0 ),0 *] by ARYTM_0:13
.= 0 by Lm2, ARYTM_0:def 7 ;
hence x * 0 = 0 ; :: thesis: verum