let D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: verum