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