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;