the Element of F * the Element of G in F ** G by Th79;
hence not F ** G is empty ; :: thesis: verum