let A, B be complex-membered set ; :: thesis: (A ** B) "" = (A "" ) ** (B "" )
let a be complex number ; :: according to MEMBERED:def 13 :: thesis: ( ( not a in (A ** B) "" or a in (A "" ) ** (B "" ) ) & ( not a in (A "" ) ** (B "" ) or a in (A ** B) "" ) )

hereby :: thesis: ( not a in (A "" ) ** (B "" ) or a in (A ** B) "" )

assume a in (A ** B) "" ; :: thesis: a in (A "" ) ** (B "" )
then consider c being Element of COMPLEX such that
A1: a = c " and
A2: c in A ** B ;
consider c1, c2 being Element of COMPLEX such that
A3: c = c1 * c2 and
A4: c1 in A and
A5: c2 in B by A2;
A6: a = (c1 " ) * (c2 " ) by A1, A3, XCMPLX_1:205;
( c1 " in A "" & c2 " in B "" ) by A4, A5;
hence a in (A "" ) ** (B "" ) by A6; :: thesis: verum

end;

assume a in (A "" ) ** (B "" ) ; :: thesis: a in (A ** B) ""
then consider c, c1 being Element of COMPLEX such that
A7: a = c * c1 and
A8: c in A "" and
A9: c1 in B "" ;
consider c2 being Element of COMPLEX such that
A10: c = c2 " and
A11: c2 in A by A8;
consider c3 being Element of COMPLEX such that
A12: c1 = c3 " and
A13: c3 in B by A9;
A14: c2 * c3 in A ** B by A11, A13;
a = (c2 * c3) " by A7, A10, A12, XCMPLX_1:205;
hence a in (A ** B) "" by A14; :: thesis: verum