consider p being FinSequence such that

A2: rng p = Y and

A3: p is one-to-one by FINSEQ_4:58;

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_{1} being Element of X ex p being FinSequence of the carrier of X st

( p is one-to-one & rng p = Y & b_{1} = the addF of X "**" p )
; :: thesis: verum

A2: rng p = Y and

A3: p is one-to-one by FINSEQ_4:58;

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

( p is one-to-one & rng p = Y & b