let x, y, z be Element of REAL+ ; :: thesis: x *' (y *' z) = (x *' y) *' z
thus x *' (y *' z) = GLUED ((DEDEKIND_CUT x) *' ((DEDEKIND_CUT y) *' (DEDEKIND_CUT z))) by Lm12
.= GLUED (((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)) *' (DEDEKIND_CUT z)) by Lm39
.= (x *' y) *' z by Lm12 ; :: thesis: verum