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