let D be non empty set ; :: thesis: for A being Matrix of 1,D holds A = <*<*(A * 1,1)*>*>
let A be Matrix of 1,D; :: thesis: A = <*<*(A * 1,1)*>*>
reconsider AA = <*<*(A * 1,1)*>*> as Matrix of 1,D by MATRIX_1:15;

now

A1: Indices A = [:(Seg 1),(Seg 1):] by MATRIX_1:25;
let i, j be Nat; :: thesis: ( [i,j] in Indices A implies AA * i,j = A * i,j )
assume A2: [i,j] in Indices A ; :: thesis: AA * i,j = A * i,j
j in {1} by A2, A1, FINSEQ_1:4, ZFMISC_1:106;
then A3: j = 1 by TARSKI:def 1;
i in {1} by A2, A1, FINSEQ_1:4, ZFMISC_1:106;
then i = 1 by TARSKI:def 1;
hence AA * i,j = A * i,j by A3, MATRIX_2:5; :: thesis: verum

end;

hence A = <*<*(A * 1,1)*>*> by MATRIX_1:28; :: thesis: verum