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

A1: Indices A = [:(Seg 2),(Seg 2):] by MATRIX_1:25;
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:4, ZFMISC_1:106;
then A3: ( j = 1 or j = 2 ) by TARSKI:def 2;
i in {1,2} by A2, A1, FINSEQ_1:4, ZFMISC_1:106;
then ( i = 1 or i = 2 ) by TARSKI:def 2;
hence AA * i,j = A * i,j by A3, MATRIX_2:6; :: thesis: verum

end;

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