theorem Th51: :: CARD_FIN:52

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