let D be non empty set ; for A being Matrix of 2,D holds A = ((A * (1,1)),(A * (1,2))) ][ ((A * (2,1)),(A * (2,2)))
let A be Matrix of 2,D; A = ((A * (1,1)),(A * (1,2))) ][ ((A * (2,1)),(A * (2,2)))
reconsider AA = ((A * (1,1)),(A * (1,2))) ][ ((A * (2,1)),(A * (2,2))) as Matrix of 2,D ;
now for i, j being Nat st [i,j] in Indices A holds
AA * (i,j) = A * (i,j)A1:
Indices A = [:(Seg 2),(Seg 2):]
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,2}
by A2, A1, FINSEQ_1:2, ZFMISC_1:87;
then A3:
(
j = 1 or
j = 2 )
by TARSKI:def 2;
i in {1,2}
by A2, A1, FINSEQ_1:2, ZFMISC_1:87;
then
(
i = 1 or
i = 2 )
by TARSKI:def 2;
hence
AA * (
i,
j)
= A * (
i,
j)
by A3, MATRIX_0:50;
verum end;
hence
A = ((A * (1,1)),(A * (1,2))) ][ ((A * (2,1)),(A * (2,2)))
by MATRIX_0:27; verum