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