let D be non empty set ; :: thesis: for A being Matrix of 1,3,D ex d1, d2, d3 being Element of D st A = <*<*d1,d2,d3*>*>
let A be Matrix of 1,3,D; :: thesis: ex d1, d2, d3 being Element of D st A = <*<*d1,d2,d3*>*>
A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>*> by Th26;
hence ex d1, d2, d3 being Element of D st A = <*<*d1,d2,d3*>*> ; :: thesis: verum