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