theorem Th23: :: BKMODEL1:26

for D being non empty set
for A being Matrix of 1,3,D holds A @ is 3,1 -size