theorem :: MATRIXR2:32

for A being Matrix of 2,REAL holds Det A = ((A * (1,1)) * (A * (2,2))) - ((A * (1,2)) * (A * (2,1)))