for x, z being ExtReal holds x * (0 + z) = (x * 0) + (x * z) by Lm25;