theorem :: BKMODEL1:31

for D being non empty set
for A being Matrix of 1,3,D holds A @ = <*<*(A * (1,1))*>,<*(A * (1,2))*>,<*(A * (1,3))*>*>