let D be non empty set ; for A being Matrix of 1,3,D holds A @ = <*<*(A * (1,1))*>,<*(A * (1,2))*>,<*(A * (1,3))*>*>
let A be Matrix of 1,3,D; A @ = <*<*(A * (1,1))*>,<*(A * (1,2))*>,<*(A * (1,3))*>*>
A1:
A @ is Matrix of 3,1,D
by Th23;
( [1,1] in Indices A & [1,2] in Indices A & [1,3] in Indices A )
by MATRIX_0:31;
then
( (A @) * (1,1) = A * (1,1) & (A @) * (2,1) = A * (1,2) & (A @) * (3,1) = A * (1,3) )
by MATRIX_0:def 6;
hence
A @ = <*<*(A * (1,1))*>,<*(A * (1,2))*>,<*(A * (1,3))*>*>
by A1, Th27; verum