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