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