theorem Th59: :: FINSEQ_4:59

for p being FinSequence st rng p c= dom p & p is one-to-one holds
rng p = dom p