assume not F ** G is empty ; :: thesis: contradiction
then the Element of F ** G in F ** G ;
then ex w1, w2 being Element of ExtREAL st
( the Element of F ** G = w1 * w2 & w1 in F & w2 in G ) ;
hence contradiction ; :: thesis: verum