consider p being FinSequence such that
A3: rng p = Y and
A4: p is one-to-one by FINSEQ_4:58;
reconsider q = p as FinSequence of DX by A3, FINSEQ_1:def 4;
ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & f "**" q = f "**" p ) by A3, A4;
hence ex b₁ being Element of DX ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b₁ = f "**" p ) ; :: thesis: verum