let x, y, z be ExtReal; :: thesis: ( y = 0 implies x * (y * z) = (x * y) * z )
assume A1: y = 0 ; :: thesis: x * (y * z) = (x * y) * z
hence x * (y * z) = 0
.= (x * y) * z by A1 ;
:: thesis: verum