let D be non empty set ; :: thesis: 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; :: thesis: 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 :: thesis: 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; :: 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,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; :: thesis: verum

end;

hence A = ((A * (1,1)),(A * (1,2))) ][ ((A * (2,1)),(A * (2,2))) by MATRIX_0:27; :: thesis: verum