theorem Th39: :: JORDAN3:39

for f, g being FinSequence of (TOP-REAL 2) st f . (len f) = g . 1 & f is being_S-Seq & g is being_S-Seq & (L~ f) /\ (L~ g) = {(g . 1)} holds
f ^ (mid (g,2,(len g))) is_S-Seq_joining f /. 1,g /. (len g)