theorem :: FINSEQ_1:100
for q being FinSubsequence holds dom (Seq q) = dom (Sgm (dom q))