reconsider f = p as Element of REAL n by EUCLID:22;
f (/) r is Element of REAL n ;
hence p (/) r is Point of (TOP-REAL n) by EUCLID:22; :: thesis: verum