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