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 Nat ) ) by NAT_1:14;
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