theorem :: EXTREAL1:2

for x, y being ExtReal
for a, b being Real st x = a & y = b holds
x / y = a / b ;