theorem :: JORDAN1J:41

for f being S-Sequence_in_R2
for g being FinSequence of (TOP-REAL 2) st g is unfolded & g is s.n.c. & g is one-to-one & (L~ f) /\ (L~ g) = {(f /. 1)} & f /. 1 = g /. (len g) & ( for i being Nat st 1 <= i & i + 2 <= len f holds
(LSeg (f,i)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {} ) & ( for i being Nat st 2 <= i & i + 1 <= len g holds
(LSeg (g,i)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {} ) holds
f ^ g is s.c.c.