let q be FinSubsequence; :: thesis: dom (Seq q) = dom (Sgm (dom q))
A1: Seq q = q * (Sgm (dom q)) by FINSEQ_1:def 14;
rng (Sgm (dom q)) = dom q by FINSEQ_1:71;
hence dom (Seq q) = dom (Sgm (dom q)) by A1, RELAT_1:46; :: thesis: verum