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:27
.= 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