theorem Th87: :: MEMBER_1:87
for f, h, i being ExtReal holds {f} ** {h,i} = {(f * h),(f * i)}