theorem :: MATRIX_0:17

for D being non empty set
for a1, a2 being Element of D holds <*<*a1,a2*>*> is Matrix of 1,2,D