:: deftheorem defines ][ MATRIX_0:def 12 :
for a, b, c, d being object holds (a,b) ][ (c,d) = <*<*a,b*>,<*c,d*>*>;