theorem :: XXREAL_3:67
for f, g being ExtReal holds (f * g) " = (f ") * (g ")