:: deftheorem defines Seq PRSUBSET:def 1 :
for x being FinSequence
for I being set holds Seq (x,I) = Seq (x | I);