:: deftheorem defines Det MATRIXR2:def 1 :
for n being Nat
for A being Matrix of n,REAL holds Det A = Det (MXR2MXF A);