theorem Th31: :: SPPOL_2:31

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