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

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

end;

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