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