let p9 be FinSubsequence; :: thesis: rng (Sgm (dom p9)) = dom p9
ex k being Nat st dom p9 c= Seg k by Def12;
hence rng (Sgm (dom p9)) = dom p9 by Def13; :: thesis: verum