theorem :: EXTREAL1:1

for x, y being ExtReal
for a, b being Real st x = a & y = b holds
x * y = a * b by XXREAL_3:def 5;