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