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