theorem Th4: :: LTLAXIO3:4

for F, G being one-to-one FinSequence st rng F misses rng G holds
F ^ G is one-to-one