assume not A ** B is empty ; :: thesis: contradiction
then the Element of A ** B in A ** B ;
then ex c1, c2 being Complex st
( the Element of A ** B = c1 * c2 & c1 in A & c2 in B ) ;
hence contradiction ; :: thesis: verum