theorem Th55: :: JORDAN1J:55

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