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