for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
( (R_Cut (f,p)) . (len (R_Cut (f,p))) = p & ( for i being Element of NAT st 1 <= i & i <= Index (p,f) holds
(R_Cut (f,p)) . i = f . i ) )