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