let x, y, z be ext-real number ; :: thesis: ( x = 0 implies x * (y * z) = (x * y) * z )
assume Z: x = 0 ; :: thesis: x * (y * z) = (x * y) * z
hence x * (y * z) = 0
.= (x * y) * z by Z ;
:: thesis: verum