theorem Th50: :: FINSEQ_1:50

for p9 being FinSubsequence holds rng (Sgm (dom p9)) = dom p9