dom (id (Seg n)) = Seg n by RELAT_1:45;
hence id (Seg n) is FinSequence-like by FINSEQ_1:def 2; :: thesis: verum