let x, z be ExtReal; :: thesis: x * (0 + z) = (x * 0) + (x * z)
thus x * (0 + z) = x * z by Th4
.= (x * 0) + (x * z) by Th4 ; :: thesis: verum