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_0:15;
now :: thesis: for i, j being Nat st [i,j] in Indices A holds
AA * (i,j) = A * (i,j)
A1: Indices A = [:(Seg 1),(Seg 1):] by MATRIX_0:24;
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:2, ZFMISC_1:87;
then A3: j = 1 by TARSKI:def 1;
i in {1} by A2, A1, FINSEQ_1:2, ZFMISC_1:87;
then i = 1 by TARSKI:def 1;
hence AA * (i,j) = A * (i,j) by A3, MATRIX_0:49; :: thesis: verum
end;
hence A = <*<*(A * (1,1))*>*> by MATRIX_0:27; :: thesis: verum