theorem Th46: :: JORDAN3:46

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
(mid (f,1,((len f) -' 1))) ^ g is_S-Seq_joining f /. 1,g /. (len g)