theorem Th88: :: MEMBER_1:88
for f, g, h, i being ExtReal holds {f,g} ** {h,i} = {(f * h),(f * i),(g * h),(g * i)}