( c1 in COMPLEX & c2 in COMPLEX ) by XCMPLX_0:def 2;
hence <%c1,c2%> is complex-valued ; :: thesis: verum