let x, z be ext-real number ; :: thesis: x * (0 + z) = (x * 0 ) + (x * z)
thus x * (0 + z) = x * z by Tx3
.= (x * 0 ) + (x * z) by Tx3 ; :: thesis: verum