theorem Th50: :: FINSEQ_1:50
for p9 being FinSubsequence holds rng (Sgm (dom p9)) = dom p9