let c1, c2 be Complex; :: thesis: Sum <%c1,c2%> = c1 + c2
( c1 in COMPLEX & c2 in COMPLEX ) by XCMPLX_0:def 2;
then addcomplex "**" <%c1,c2%> = addcomplex . (c1,c2) by Th38
.= c1 + c2 by BINOP_2:def 3 ;
hence Sum <%c1,c2%> = c1 + c2 ; :: thesis: verum