theorem Th25: :: BKMODEL1:28

for D being non empty set
for d1, d2, d3 being Element of D holds <*<*d1*>,<*d2*>,<*d3*>*> is Matrix of 3,1,D