let D be non empty set ; :: thesis: for M being Matrix of 1,D holds M = <*<*(M * (1,1))*>*>
let M be Matrix of 1,D; :: thesis: M = <*<*(M * (1,1))*>*>
A1: ( Indices M = [:(Seg 1),(Seg 1):] & 1 in Seg 1 ) by FINSEQ_1:2, MATRIX_0:24, TARSKI:def 1;
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = <*<*(M * (1,1))*>*> * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices M implies M * (i,j) = <*<*(M * (1,1))*>*> * (i,j) )
assume [i,j] in Indices M ; :: thesis: M * (i,j) = <*<*(M * (1,1))*>*> * (i,j)
then ( i in Seg 1 & j in Seg 1 ) by A1, ZFMISC_1:87;
then ( i = 1 & j = 1 ) by FINSEQ_1:2, TARSKI:def 1;
hence M * (i,j) = <*<*(M * (1,1))*>*> * (i,j) by MATRIX_0:49; :: thesis: verum

end;

hence M = <*<*(M * (1,1))*>*> by MATRIX_0:27; :: thesis: verum