for f, h, i being ExtReal holds {f} ** {h,i} = {(f * h),(f * i)}