let x, y be ext-real number ; :: thesis: x * (y + y) = (x * y) + (x * y)
thus x * (y + y) = x * (2 * y) by Th105
.= 2 * (x * y) by Th77
.= (x * y) + (x * y) by Th105 ; :: thesis: verum