let n be Nat; :: thesis: for K being Field
for N being Matrix of n,K holds Det <*N*> = <*(Det N)*>
let K be Field; :: thesis: for N being Matrix of n,K holds Det <*N*> = <*(Det N)*>
let N be Matrix of n,K; :: thesis: Det <*N*> = <*(Det N)*>
set F = <*N*>;
A1: ( len <*N*> = 1 & 1 in Seg 1 ) by FINSEQ_1:57;
A2: ( dom (Det <*N*>) = Seg (len <*N*>) & len <*N*> = len (Det <*N*>) ) by FINSEQ_1:def 18, FINSEQ_2:144;
( (Det <*N*>) . 1 = Det (<*N*> . 1) & <*N*> . 1 = N & n = len N ) by A1, A2, Def7, FINSEQ_1:57, MATRIX_1:def 3;
hence Det <*N*> = <*(Det N)*> by A1, A2, FINSEQ_1:57; :: thesis: verum