:: deftheorem defines Seq FINSEQ_1:def 15 :
for p being FinSubsequence holds Seq p = p * (Sgm (dom p));