for F being ext-real-membered set
for f being ExtReal holds f ** F = { (f * w) where w is Element of ExtREAL : w in F }