let x, y, z be Real; :: thesis: ((1 / x) * (1 / y)) * (1 / z) = 1 / ((x * y) * z)
((1 / x) * (1 / y)) * (1 / z) = (1 / (x * y)) * (1 / z) by XCMPLX_1:102
.= 1 / ((x * y) * z) by XCMPLX_1:102 ;
hence ((1 / x) * (1 / y)) * (1 / z) = 1 / ((x * y) * z) ; :: thesis: verum