:: deftheorem defines <* FINSEQ_4:def 8 :
for x1, x2, x3, x4, x5 being object holds <*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*>;