let D be non empty set ; :: thesis: for M being Matrix of 1,D holds M @ = M
let M be Matrix of 1,D; :: thesis: M @ = M
A1: M = <*<*(M * (1,1))*>*> by MATRIX13:20;
Indices M = [:{1},{1}:] by MATRIX_0:24, FINSEQ_1:2;
then [1,1] in Indices M by ZFMISC_1:28;
then (M @) * (1,1) = M * (1,1) by MATRIX_0:def 6;
hence M @ = M by A1, MATRIX13:20; :: thesis: verum