:: deftheorem defines addcr FINSEQ_8:def 11 :
for D being non empty set
for f, CR being FinSequence of D holds addcr (f,CR) = ovlcon (f,CR);