theorem :: FINSEQ_1:100

for q being FinSubsequence holds dom (Seq q) = dom (Sgm (dom q))