let x, y, z be ExtReal; :: thesis: x * (y * z) = (x * y) * z

per cases ( ( x is real & y is real & z is real ) or not x is real or not z is real or not y is real ) ;

suppose ( x is real & y is real & z is real ) ; :: thesis: x * (y * z) = (x * y) * z

then reconsider r = x, s = y, t = z as Real ;
reconsider rs = r * s, sx = s * t as Real ;
thus x * (y * z) = r * sx
.= rs * t
.= (x * y) * z ; :: thesis: verum

end;

suppose ( not x is real or not z is real ) ; :: thesis: x * (y * z) = (x * y) * z

hence x * (y * z) = (x * y) * z by Lm22; :: thesis: verum

end;

suppose not y is real ; :: thesis: x * (y * z) = (x * y) * z

hence x * (y * z) = (x * y) * z by Lm21; :: thesis: verum

end;

end;