for n being Nat
for A being Matrix of n,REAL holds Det A = Det (A @) by Th43;