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