assume A1: ( A = F & B = G ) ; :: thesis: A ** B = F ** G
let a be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not a in A ** B or a in F ** G ) & ( not a in F ** G or a in A ** B ) )

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

assume a in A ** B ; :: thesis: a in F ** G
then consider c, c1 being Complex such that
A2: a = c * c1 and
A3: ( c in A & c1 in B ) ;
reconsider d1 = c, d2 = c1 as Element of ExtREAL by A3, XXREAL_0:def 1;
a = d1 * d2 by A2, A3, XXREAL_3:def 5;
hence a in F ** G by A1, A3; :: thesis: verum

end;

assume a in F ** G ; :: thesis: a in A ** B
then consider w, w1 being Element of ExtREAL such that
A4: a = w * w1 and
A5: ( w in F & w1 in G ) ;
reconsider d1 = w, d2 = w1 as Element of COMPLEX by A1, A5, XCMPLX_0:def 2;
a = d1 * d2 by A1, A4, A5, XXREAL_3:def 5;
hence a in A ** B by A1, A5; :: thesis: verum