theorem Th1: :: HILB10_2:1

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