:: deftheorem defines <* NOMIN_9:def 2 :
for a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 being object holds <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> = <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> ^ <*a10*>;