let A, B be complex-membered set ; :: thesis: (A ** B) "" = (A "") ** (B "")
let a be Complex; :: 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 Complex such that
A1: a = c " and
A2: c in A ** B ;
consider c1, c2 being Complex such that
A3: c = c1 * c2 and
A4: ( c1 in A & c2 in B ) by A2;
A5: ( c1 " in A "" & c2 " in B "" ) by A4;
a = (c1 ") * (c2 ") by A1, A3, XCMPLX_1:204;
hence a in (A "") ** (B "") by A5; :: thesis: verum
end;
assume a in (A "") ** (B "") ; :: thesis: a in (A ** B) ""
then consider c, c1 being Complex such that
A6: a = c * c1 and
A7: c in A "" and
A8: c1 in B "" ;
consider c3 being Complex such that
A9: c1 = c3 " and
A10: c3 in B by A8;
consider c2 being Complex such that
A11: c = c2 " and
A12: c2 in A by A7;
A13: c2 * c3 in A ** B by A12, A10;
a = (c2 * c3) " by A6, A11, A9, XCMPLX_1:204;
hence a in (A ** B) "" by A13; :: thesis: verum