theorem :: MEMBER_1:113

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