let n be Element of NAT ; :: thesis: for A being Matrix of n, REAL holds Det A = Det (A @ )
let A be Matrix of n, REAL ; :: thesis: Det A = Det (A @ )
reconsider N1 = MXR2MXF A, N2 = MXR2MXF (A @ ) as Matrix of n,F_Real ;
reconsider N3 = MXF2MXR (N1 @ ) as Matrix of n, REAL ;
reconsider N4 = MXR2MXF N3 as Matrix of n,F_Real ;
N4 = N2 by MATRIX_7:def 3;
hence Det A = Det (A @ ) by Th43; :: thesis: verum