let I, J be set ; :: thesis: ( J in Fin I implies ex p being FinSequence of I st

( J = rng p & p is one-to-one ) )

assume A1: J in Fin I ; :: thesis: ex p being FinSequence of I st

( J = rng p & p is one-to-one )

consider p being FinSequence such that

A2: ( J = rng p & p is one-to-one ) by A1, FINSEQ_4:58;

rng p c= I by A1, A2, FINSUB_1:def 5;

then reconsider p = p as FinSequence of I by FINSEQ_1:def 4;

take p ; :: thesis: ( J = rng p & p is one-to-one )

thus ( J = rng p & p is one-to-one ) by A2; :: thesis: verum

( J = rng p & p is one-to-one ) )

assume A1: J in Fin I ; :: thesis: ex p being FinSequence of I st

( J = rng p & p is one-to-one )

consider p being FinSequence such that

A2: ( J = rng p & p is one-to-one ) by A1, FINSEQ_4:58;

rng p c= I by A1, A2, FINSUB_1:def 5;

then reconsider p = p as FinSequence of I by FINSEQ_1:def 4;

take p ; :: thesis: ( J = rng p & p is one-to-one )

thus ( J = rng p & p is one-to-one ) by A2; :: thesis: verum