let x, y be ExtReal; :: thesis: x * (y + y) = (x * y) + (x * y)
thus x * (y + y) = x * (2 * y) by Th94
.= 2 * (x * y) by Th66
.= (x * y) + (x * y) by Th94 ; :: thesis: verum