thus X --> r is PartFunc of X, REAL ; :: thesis: verum