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