reconsider a9 = a, b9 = b as Element of COMPLEX by XCMPLX_0:def 2;
assume ( x = a & y = b ) ; :: thesis: x + y = a + b
hence x + y = addcomplex . (a9,b9) by Def1
.= a + b by BINOP_2:def 3 ;
:: thesis: verum