:: deftheorem defines -: FINSEQ_5:def 1 :
for D being non empty set
for f being FinSequence of D
for p being set holds f -: p = f | (p .. f);