let a, b be Complex; :: thesis: {a} ** {b} = {(a * b)}
let z be Complex; :: according to MEMBERED:def 13 :: thesis: ( ( not z in {a} ** {b} or z in {(a * b)} ) & ( not z in {(a * b)} or z in {a} ** {b} ) )

hereby :: thesis: ( not z in {(a * b)} or z in {a} ** {b} )

assume z in {a} ** {b} ; :: thesis: z in {(a * b)}
then consider c1, c2 being Complex such that
A1: z = c1 * c2 and
A2: ( c1 in {a} & c2 in {b} ) ;
( c1 = a & c2 = b ) by A2, TARSKI:def 1;
hence z in {(a * b)} by A1, TARSKI:def 1; :: thesis: verum

end;

A3: ( a in {a} & b in {b} ) by TARSKI:def 1;
assume z in {(a * b)} ; :: thesis: z in {a} ** {b}
then A4: z = a * b by TARSKI:def 1;
thus z in {a} ** {b} by A4, A3; :: thesis: verum