for p being FinSequence of 1 -tuples_on REAL st len p = 3 holds
M2F p is Point of (TOP-REAL 3)