ex p being FinSequence st
( rng p = X & p is one-to-one ) by FINSEQ_4:58;
hence ex b₁ being one-to-one FinSequence st rng b₁ = X ; :: thesis: verum