theorem :: MEMBER_1:114

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