rng (Sgm (dom p9)) = dom p9 by Th50;
then dom (p9 * (Sgm (dom p9))) = dom (Sgm (dom p9)) by RELAT_1:27
.= Seg (len (Sgm (dom p9))) by Def3 ;
hence Seq p9 is FinSequence-like ; :: thesis: verum