let q be FinSubsequence; :: thesis: dom (Seq q) = dom (Sgm (dom q))
rng (Sgm (dom q)) = dom q by Th50;
hence dom (Seq q) = dom (Sgm (dom q)) by RELAT_1:27; :: thesis: verum