let K be Field; :: thesis: for n being Nat
for A being Matrix of n,K holds Det A = Det (A @ )
let n be Nat; :: thesis: for A being Matrix of n,K holds Det A = Det (A @ )
let A be Matrix of n,K; :: thesis: Det A = Det (A @ )
( n = 0 or ( n >= 1 & n is Element of NAT ) ) by NAT_1:14, ORDINAL1:def 13;
then ( ( Det A = 1_ K & Det (A @ ) = 1_ K ) or Det A = Det (A @ ) ) by Th41, MATRIX_7:37;
hence Det A = Det (A @ ) ; :: thesis: verum