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