let x, y, z be ext-real number ; :: 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 number ;
reconsider rs = r * s, sx = s * t as real number ;
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 LmB; :: thesis: verum

end;

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

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

end;

end;