theorem Th30: :: SPPOL_2:30

for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for k being Nat st f is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),p)) = {(f /. (len f))} holds
f ^ <*p*> is unfolded