reconsider q = p as Element of dom t by A1;
rng (q succ ) c= dom t ;
then dom (t * (q succ )) = dom (q succ ) by RELAT_1:46
.= Seg (len (q succ )) by FINSEQ_1:def 3 ;
then t * (q succ ) is FinSequence by FINSEQ_1:def 2;
hence ex b₁ being FinSequence ex q being Element of dom t st
( q = p & b₁ = t * (q succ ) ) ; :: thesis: verum