reconsider p' = p as Element of REAL n ;
x * p' is Point of (TOP-REAL n) ;
hence x * p is Point of (TOP-REAL n) ; :: thesis: verum