theorem Th54: :: JORDAN1J:54

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