:: deftheorem defines <* FINSEQ_1:def 10 :
for x, y, z being object holds <*x,y,z*> = (<*x*> ^ <*y*>) ^ <*z*>;