:: deftheorem defines <* AOFA_A00:def 4 :
for a1, a2, a3, a4, a5, a6, a7 being object holds <*a1,a2,a3,a4,a5,a6,a7*> = <*a1,a2,a3,a4,a5*> ^ <*a6,a7*>;