reconsider r = r as Element of REAL by XREAL_0:def 1;
X --> r is PartFunc of X,REAL ;
hence X --> r is PartFunc of X,REAL ; :: thesis: verum