let A be Matrix of 2, REAL ; :: thesis: Det A = ((A * 1,1) * (A * 2,2)) - ((A * 1,2) * (A * 2,1))
reconsider N = MXR2MXF A as Matrix of 2,F_Real ;
Det A = ((N * 1,1) * (N * 2,2)) - ((N * 1,2) * (N * 2,1)) by MATRIX_7:12;
hence Det A = ((A * 1,1) * (A * 2,2)) - ((A * 1,2) * (A * 2,1)) ; :: thesis: verum