theorem Th89: :: FINSEQ_3:91

for p, q being FinSequence holds
( ( rng p misses rng q & p is one-to-one & q is one-to-one ) iff p ^ q is one-to-one )