:: deftheorem defines ** MEMBER_1:def 9 :
for F, G being ext-real-membered set holds F ** G = { (w1 * w2) where w1, w2 is Element of ExtREAL : ( w1 in F & w2 in G ) } ;