:: deftheorem defines <* FINSEQ_1:def 9 :
for x, y being object holds <*x,y*> = <*x*> ^ <*y*>;