let D be non empty set ; for A being Matrix of 1,D holds A = <*<*(A * (1,1))*>*>
let A be Matrix of 1,D; A = <*<*(A * (1,1))*>*>
reconsider AA = <*<*(A * (1,1))*>*> as Matrix of 1,D by MATRIX_0:15;
now 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;
( [i,j] in Indices A implies AA * (i,j) = A * (i,j) )assume A2:
[i,j] in Indices A
;
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;
verum end;
hence
A = <*<*(A * (1,1))*>*>
by MATRIX_0:27; verum