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

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies AA * i,j = A * i,j )
assume A1: [i,j] in Indices A ; :: thesis: AA * i,j = A * i,j
Indices A = [:(Seg 2),(Seg 2):] by MATRIX_1:25;
then ( i in {1,2} & j in {1,2} ) by A1, FINSEQ_1:4, ZFMISC_1:106;
then ( ( i = 1 or i = 2 ) & ( j = 1 or j = 2 ) ) by TARSKI:def 2;
hence AA * i,j = A * i,j by 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